tensorDistribEquiv_apply — Mathlib

English

The base change operation maps a bilinear form on M2 over R to a bilinear form on A ⊗ M2 over A.

Русский

Операция базового изменения переводит билинейную форму на M2 над R в билинейную форму на A ⊗ M2 над A.

LaTeX

$$$$ LinearMap.BilinForm.baseChange (B : BilinForm R M_2) : BilinForm A (A \otimes_R M_2). $$$$

Lean4

@[simp]
theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) :
    tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B :=
  DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B

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