baseChange_tmul — Mathlib

English

Evaluating the base change on simple tensors yields a product of scalars in the base ring.

Русский

Оценка базового изменения на простых тензорах даёт произведение скаляров базового кольца.

LaTeX

$$$$ B_2.baseChange\\; A\\ (a \\otimes m_2)\ (a' \\otimes m_2') = (B_2(m_2,m_2')) \\cdot (a a'). $$$$

Lean4

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

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