Theorems · Definition · linear algebra

Submodule.dualCoannihilator

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

The dualAnnihilator of a submodule of the dual space pulled back along the evaluation map Module.Dual.eval.

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

41 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule