refl — Mathlib

English

The coercion of the identity-related ContinuousMulEquiv refl is equal to the identity map.

Русский

Приведение равносильно рефлексии к функции совпадает с тождественной перестановкой.

LaTeX

$$$\!\uparrow(\mathrm{refl}\,M)=\mathrm{id}$$$

Lean4

/-- The identity map is a continuous multiplicative isomorphism. -/
@[to_additive (attr := refl) /-- The identity map is a continuous additive isomorphism. -/
    ]
def refl : M ≃ₜ* M :=
  { MulEquiv.refl _ with
    continuous_toFun := by dsimp; fun_prop
    continuous_invFun := by dsimp; fun_prop }

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