baseChange — Mathlib

English

The polar bilinear form is compatible with base change: polarBilin(baseChange Q) = baseChange(polarBilin(Q)).

Русский

Полярная билинейная форма совместима с базовым изменением: polarBilin(baseChange(Q)) = baseChange(polarBilin(Q)).

LaTeX

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

Lean4

/-- The base change of a quadratic form. -/
protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
  QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticMap.sq (R := A)) Q

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