baseChange_tmul — Mathlib

English

The associated quadratic form commutes with base change: associated(baseChange Q) equals baseChange of associated Q.

Русский

Связанные формы и базовое изменение коммутируют: associated(baseChange(Q)) = baseChange(associated(Q)).

LaTeX

$$$\\text{associated}(\\text{baseChange } A\, Q) = \\text{BilinForm.baseChange } A (\\text{associated}(Q))$$$

Lean4

@[simp]
theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : Q.baseChange A (a ⊗ₜ m₂) = Q m₂ • (a * a) :=
  tensorDistrib_tmul _ _ _ _

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