refl — Mathlib

English

A group extension is equivalent to itself via the identity equivalence.

Русский

Групповое расширение эквивалентно самому себе через тождественную эквивалентность.

LaTeX

$$$\\mathrm{refl} : S.\\Equiv S$$$

Lean4

/-- A group extension is equivalent to itself. -/
@[to_additive (attr := simps!) /-- An additive group extension is equivalent to itself. -/
    ]
def refl : S.Equiv S where
  __ := MulEquiv.refl E
  inl_comm := rfl
  rightHom_comm := rfl

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