Theorems · Theorem · linear algebra
Submodule.span_singleton_le_iff_mem
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
(p : Submodule R M), R ∙ m ≤ p ↔ m ∈ p- Defined in
- Mathlib.LinearAlgebra.Span.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Submodulestatement and proof · cited by 7,192
- Submodule.spanstatement · cited by 1,504
- SetLike.mem_coeproof · cited by 302
- Set.singleton_subset_iffproof · cited by 206
- Submodule.span_leproof · cited by 164
Cited by21
Results whose statement or proof uses this declaration.
- Algebra.Generators.Cotangent.exactproof · cited by 6
- Ideal.isIdempotentElem_iff_of_fgproof · cited by 5
- FractionalIdeal.spanSingleton_le_iff_memproof · cited by 3
- Module.isPrincipal_submodule_iffproof · cited by 1
- dvd_generator_iffproof · cited by 1
- isNoetherian_iff_fg_wellFoundedproof · cited by 1
- Affine.Simplex.sum_inv_height_sq_smul_vsub_eq_zeroproof · cited by 1
- Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilatorproof · cited by 1
- LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizerproof · cited by 1
- Submodule.isQuotientEquivQuotientPrime_iffproof · cited by 1
- FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_topproof · cited by 1
- AffineSubspace.direction_affineSpan_pair_le_iff_exists_smulproof · cited by 1