dualPairing_apply — Mathlib

English

There is a canonical linear equivalence between the dual of the quotient M/W and the dual annihilator W.dualAnnihilator, i.e., (M/W)^* ≃ W.dualAnnihilator.

Русский

Существует каноническое линейное эквивалентное соответствие между двойственностью модуля M/W и двойственным аннигилятором W.dualAnnihilator: (M/W)^* ≃ W.dualAnnihilator.

LaTeX

$$$\text{dualQuotEquivDualAnnihilator} (W) : (M/W)^* \cong W.dualAnnihilator$$$

Lean4

@[simp]
theorem dualPairing_apply {W : Submodule R M} (φ : Module.Dual R M) (x : W) : W.dualPairing (Quotient.mk φ) x = φ x :=
  rfl

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