baseChange_tmul — Mathlib

English

For B2 symmetric, B2.baseChange is symmetric with respect to tmul, i.e., B2.baseChange A x y = B2.baseChange A y x for appropriate x,y.

Русский

Для симметричной B2 отображение baseChange сохраняет симметрию относительно tmul.

LaTeX

$$$B_2.baseChange\\ A x y = B_2.baseChange\\ A y x$$$

Lean4

@[simp]
theorem baseChange_tmul (B₂ : BilinMap R M₂ N₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) :
    B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂') :=
  rfl

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