equivOfIsometry_refl — Mathlib

English

The isometry corresponding to the identity isometry yields the identity algebra isomorphism: equivOfIsometry (refl Q1) = AlgEquiv.refl.

Русский

Изометрия, соответствующая тождественному отображению, порождает тождественный алгебраический эквивалент: equivOfIsometry (refl Q1) = AlgEquiv.refl.

LaTeX

$$$ (\mathrm{equivOfIsometry} (\mathrm{QuadraticMap.IsometryEquiv.refl} Q_1)) = \mathrm AlgEquiv.refl $.$$

Lean4

@[simp]
theorem equivOfIsometry_refl : (equivOfIsometry <| QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl :=
  by
  ext x
  exact AlgHom.congr_fun (map_id Q₁) x

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