dualSubmoduleParing — Mathlib

English

For x ∈ B.dualSubmodule N and y ∈ N, the algebra map from R to S sends B.dualSubmoduleParing x y to B(x,y), i.e., algebraMap_R_S(B.dualSubmoduleParing x y) = B(x,y).

Русский

Для x ∈ дуальной подмодуля и y ∈ N выполняется: algebraMap_R_S(B.dualSubmoduleParing x y) = B(x,y).

LaTeX

$$$$ \mathrm{algebraMap}_{R\to S}( \mathrm{B.dualSubmoduleParing}(x,y) ) = B(x,y). $$$$

Lean4

/-- The natural paring of `B.dualSubmodule N` and `N`.
This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`. -/
noncomputable def dualSubmoduleParing {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : R :=
  (Submodule.mem_one.mp <| x.prop y y.prop).choose

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