dualSubmoduleParing_spec — Mathlib

English

The natural pairing of B.dualSubmodule N and N gives a linear map from B.dualSubmodule N to the Module.Dual_R N, i.e., x ↦ (y ↦ B(x,y)).

Русский

Естественная парная связь между B.dualSubmodule N и N задаёт линейное отображение из B.dualSubmodule N в Moduled Dual_R N: x ↦ (y ↦ B(x,y)).

LaTeX

$$$$ B.dualSubmoduleToDual(N) : B.dualSubmodule N \to \mathrm{Module.Dual}_R N, \quad x \mapsto (y \mapsto B(x,y)). $$$$

Lean4

@[simp]
theorem dualSubmoduleParing_spec {N : Submodule R M} (x : B.dualSubmodule N) (y : N) :
    algebraMap R S (B.dualSubmoduleParing x y) = B x y :=
  (Submodule.mem_one.mp <| x.prop y y.prop).choose_spec

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