symm — Mathlib

English

The inverse isometric equivalence of an isometric equivalence between two quadratic forms.

Русский

Обратная изометрическая эквивалентность изометрического эквивалентного отображения между квадратичными формами.

LaTeX

$$$\mathrm{symm}(f) : Q_2.\IsometryEquiv Q_1$ from $Q_1.\IsometryEquiv Q_2$$$

Lean4

/-- The inverse isometric equivalence of an isometric equivalence between two quadratic forms. -/
@[symm]
def symm (f : Q₁.IsometryEquiv Q₂) : Q₂.IsometryEquiv Q₁ :=
  { (f : M₁ ≃ₗ[R] M₂).symm with
    map_app' := by intro m; rw [← f.map_app]; congr; exact f.toLinearEquiv.apply_symm_apply m }

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