freeGroupCongr_refl — Mathlib

English

The identity equivalence gives the identity Morita (MulEquiv) on FreeGroup: freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α).

Русский

Единичная эквивалентность порождает тождественную мультиэквивалентность между свободными группами: freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α).

LaTeX

$$$ freeGroupCongr\\ (Equiv.refl\\ α) = MulEquiv.refl\\ (FreeGroup\\ α) $$$

Lean4

@[to_additive (attr := simp)]
theorem freeGroupCongr_refl : freeGroupCongr (Equiv.refl α) = MulEquiv.refl _ :=
  MulEquiv.ext map.id

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