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 }