associated_flip — Mathlib

English

The flip of the associatedHom map equals the associatedHom map itself for any Q.

Русский

Поворот (flip) ассоциированного отображения равен самому ассоциированному отображению.

LaTeX

$$$ (associatedHom S Q).flip = associatedHom S Q $$$

Lean4

/-- A version of `QuadraticMap.associated_isSymm` for general targets
(using `flip` because `IsSymm` does not apply here). -/
theorem associated_flip : (associatedHom S Q).flip = associatedHom S Q :=
  by
  ext
  simp only [LinearMap.flip_apply, associated_apply, add_comm, sub_eq_add_neg, add_left_comm, add_assoc]

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