baseChange_isSymm — Mathlib

English

Another formulation: if B2 is symmetric, the baseChange operation yields a symmetric bilinear form on the extended space.

Русский

Еще одно формулирование: если B2 симметрична, операция baseChange задаёт симметричную билинейную форму на расширенном пространстве.

LaTeX

$$$(B_2.baseChange\\ A)\\text{ is symmetric}$$$

Lean4

theorem baseChange_isSymm {B₂ : BilinMap R M₂ N₂} (hB₂ : ∀ x y, B₂ x y = B₂ y x) (x y : A ⊗[R] M₂) :
    B₂.baseChange A x y = B₂.baseChange A y x :=
  tmul_isSymm mul_comm hB₂ x y

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