isometryEquivOfCompLinearEquiv — Mathlib

English

A quadratic form composed with a linear equivalence is isometric to itself, via the natural pullback along the inverse linear equivalence.

Русский

Квадратичная форма, составленная с линейным эквивалентом, изометрична самой себе через обратное линейное эквивалентное отображение.

LaTeX

$$$Q \circ f \;\text{is isometric to } Q$, i.e., $Q.IsometryEquiv(Q.comp(f))$ with the given construction.$$

Lean4

/-- A quadratic form composed with a `LinearEquiv` is isometric to itself. -/
def isometryEquivOfCompLinearEquiv (Q : QuadraticMap R M N) (f : M₁ ≃ₗ[R] M) :
    Q.IsometryEquiv (Q.comp (f : M₁ →ₗ[R] M)) :=
  { f.symm with
    map_app' := by
      intro
      simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe, f.apply_symm_apply] }

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