English
The composition of monoid isomorphisms associated to equivalences of group extensions gives another equivalence.
Русский
Составимость моноидных изоморфизмов, соответствующих эквивалентностям групповых расширений, образует другую эквивалентность.
LaTeX
$$${equiv}.trans {equiv'} : S.\\Equiv S''$$$
Lean4
/-- The composition of monoid isomorphisms associated to equivalences of group extensions gives
another equivalence. -/
@[to_additive (attr := simps!) /-- The composition of monoid isomorphisms associated to equivalences of additive group
extensions gives another equivalence. -/
]
def trans {E'' : Type*} [Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') : S.Equiv S''
where
__ := equiv.toMulEquiv.trans equiv'.toMulEquiv
inl_comm := by rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]
rightHom_comm := by rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]
