baseChange — Mathlib

English

Changing the ground ring via an algebra A produces a base-changed bilinear form on A ⊗_R M.

Русский

Переход базиса по основаниям через A даёт билинейную форму на A ⊗_R M.

LaTeX

$$$$ (B: BilinForm\; R\; M) \mapsto (B:\ BilinForm\; A\; (A \otimes_R M)) $$$$

Lean4

/-- The base change of a bilinear form. -/
protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) :=
  BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B

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