Theorems · Definition · linear algebra

Submodule.dualAnnihilator

{R : Type u_3} →
  {M : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Submodule R (Module.Dual R M)

The dualAnnihilator of a submodule W is the set of linear maps φ such that φ w = 0 for all w ∈ W.

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

77 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule