associated_baseChange — Mathlib

English

The tmul operation is compatible with base change: tmul (Q1) (Q2) under base change equals the tmul of base-changed Q1 and Q2.

Русский

tmul совместим с базовым изменением: tmul (Q1) (Q2) при базовом изменении равно tmul базируемых Q1 и Q2.

LaTeX

$$$\\text{tmul} \\, (\\text{baseChange } A\, Q_1) \; (Q_2) = \\text{baseChange}(\\text{tmul}(Q_1,Q_2))$$$

Lean4

theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
    associated (R := A) (Q.baseChange A) = BilinForm.baseChange A (associated (R := R) Q) :=
  by
  dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]
  rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]
  exact rfl

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