dualAnnihilator — Mathlib

English

If R is a domain, then for any module M over R, NoZeroSMulDivisors(R,M) holds.

Русский

Если R — домен, тогда для любого модуля M над R выполняется свойство NoZeroSMulDivisors(R,M).

LaTeX

$$[IsDomain(R)] ⇒ NoZeroSMulDivisors(R,M).$$

Lean4

/-- The `dualAnnihilator` of a submodule `W` is the set of linear maps `φ` such
  that `φ w = 0` for all `w ∈ W`. -/
def dualAnnihilator {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) :
    Submodule R <| Module.Dual R M :=
  LinearMap.ker W.dualRestrict

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