refl_symm — Mathlib

English

The inverse of the identity ordered monoid isomorphism is the identity isomorphism: (refl α).symm = refl α.

Русский

Обратное отображение тождественного упорядоченного изоморфизма равно тождественному отображению: (refl α).symm = refl α.

LaTeX

$$$(\\mathrm{refl}\\,\\alpha)^{\\mathrm{symm}} = \\mathrm{refl}\\,\\alpha$$$

Lean4

@[to_additive (attr := simp)]
theorem refl_symm : (OrderMonoidIso.refl α).symm = .refl α :=
  rfl

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