compBilinForm — Mathlib

English

With a finite basis b, B.dualSubmodule (B.flip.dualSubmodule(span_R(range b))) = span_R(range b).

Русский

При конечном базисе b выполняется B.dualSubmodule(B.flip.dualSubmodule(span_R(range b))) = span_R(range b).

LaTeX

$$$$ B.dualSubmodule( B.flip.dualSubmodule(\mathrm{span}_R(\mathrm{range}\, b)) ) = \mathrm{span}_R(\mathrm{range}\, b). $$$$

Lean4

/-- Apply a linear map on the output of a bilinear form. -/
@[simps!]
def compBilinForm (f : R →ₗ[R'] R') (B : BilinForm R M) : BilinForm R' M :=
  compr₂ (restrictScalars₁₂ R' R' B) f

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