Theorems · Theorem · linear algebra

Submodule.span_eq_top_of_ne_zero

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.IsReflexive R M] {s : Set (M →ₗ[R] R)} [Module.Projective R ((M →ₗ[R] R) ⧸ Submodule.span R s)],
  (∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0) → Submodule.span R s = ⊤

Consider a reflexive module and a set s of linear forms. If for any z ≠ 0 there exists f ∈ s such that f z ≠ 0, then s spans the whole dual space.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.IsReflexiveModule.Projective