English
For a suitably symmetric B, the orthogonality of the associated quadratic map agrees with the orthogonality of B.
Русский
Для симметричной билинейной формы B орторгониальность ассоциированной квадратичной карты совпадает с орторгониальностью B.
LaTeX
$$$\\forall B,x,y:\\;\\text{B.IsSymm} \\Rightarrow (B.toQuadraticMap.IsOrtho x y \\iff B.IsOrtho x y).$$$
Lean4
theorem _root_.LinearMap.BilinForm.toQuadraticMap_isOrtho [IsCancelAdd R] [NoZeroDivisors R] [CharZero R]
{B : BilinMap R M R} {x y : M} (h : B.IsSymm) : B.toQuadraticMap.IsOrtho x y ↔ B.IsOrtho x y :=
by
letI : AddCancelMonoid R := { ‹IsCancelAdd R›, (inferInstanceAs <| AddCommMonoid R) with }
simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add, LinearMap.add_apply, add_comm _ (B y y),
add_add_add_comm _ _ (B y y), add_comm (B y y)]
rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
