refl — Mathlib

English

The identity isometric equivalence between a quadratic form and itself.

Русский

Идентичноe изометрическое эквивалент между квадратичной формой и самой собой.

LaTeX

$$$\mathrm{refl}(Q) : Q \IsometryEquiv Q$$$

Lean4

/-- The identity isometric equivalence between a quadratic form and itself. -/
@[refl]
def refl (Q : QuadraticMap R M N) : Q.IsometryEquiv Q :=
  { LinearEquiv.refl R M with map_app' := fun _ => rfl }

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