symm — Mathlib

English

Right-hand homs commute with the equivalence, i.e., S'.rightHom (equiv e) = S.rightHom e.

Русский

Правые гомоморфизмы коммутируют с эквивалентностью: S'.rightHom (equiv e) = S.rightHom e.

LaTeX

$$$S'.rightHom (equiv e) = S.rightHom e$$$

Lean4

/-- The inverse of an equivalence of group extensions is an equivalence. -/
@[to_additive /-- The inverse of an equivalence of additive group extensions is an equivalence. -/
    ]
def symm : S'.Equiv S where
  __ := equiv.toMulEquiv.symm
  inl_comm := by rw [MulEquiv.symm_comp_eq, ← equiv.inl_comm]
  rightHom_comm := by rw [MulEquiv.comp_symm_eq, ← equiv.rightHom_comm]

Похожие утверждения