associated_isSymm — Mathlib

English

The abbrev associated' gives a canonical ℤ-linear map from QuadraticMap to BilinMap, showing the symmetry of the construction.

Русский

Обозначение associated' задаёт стандартную ℤ-линейную отображение от QuadraticMap к BilinMap, фиксируя симметрию конструкции.

LaTeX

$$$ associated' : QuadraticMap R M N \to BilinMap R M N $$$

Lean4

theorem associated_isSymm (Q : QuadraticMap R M N) (x y : M) : associatedHom S Q x y = associatedHom S Q y x := by
  simp only [associated_apply, sub_eq_add_neg, add_assoc, add_comm, add_left_comm]

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