Composition and OrderMonoidIso.withZero

Mathlib's OrderMonoidIso.withZero identifies order isomorphisms of two ordered groups with order isomorphisms of those groups with a zero adjoined. This file records that its inverse is compatible with composition, the analogue of Equiv.optionCongr_trans.

Main results

• OrderMonoidIso.withZero_symm_trans: the inverse of OrderMonoidIso.withZero sends a composite to the composite of the images.

@[simp]

theorem OrderMonoidIso.withZero_symm_trans {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [PartialOrder G] [Group H] [PartialOrder H] [Group K] [PartialOrder K] (A : WithZero G ≃*o WithZero H) (B : WithZero H ≃*o WithZero K) : (withZero.symm A).trans (withZero.symm B) = withZero.symm (A.trans B)

The inverse of OrderMonoidIso.withZero is compatible with composition.