Theorems · Theorem · commutative algebra
Submodule.sub_mem
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x y : M}, x ∈ p → y ∈ p → x - y ∈ p- Defined in
- Mathlib.Algebra.Module.Submodule.Defs
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- RingAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- sub_memproof · cited by 40
Cited by43
Results whose statement or proof uses this declaration.
- direction_affineSpanproof · cited by 46
- Ideal.sub_memproof · cited by 22
- AffineSubspace.direction_mk'proof · cited by 15
- Submodule.fg_of_fg_map_of_fg_inf_kerproof · cited by 7
- vectorSpan_eq_span_vsub_set_rightproof · cited by 7
- Submodule.eq_starProjection_of_mem_of_inner_eq_zeroproof · cited by 6
- vectorSpan_eq_span_vsub_set_leftproof · cited by 4
- range_derivWithin_subset_closure_span_imageproof · cited by 3
- MeasureTheory.Measure.addHaar_submoduleproof · cited by 3
- LinearMap.restrict_substatement · cited by 3
- Submodule.basis_of_pid_auxproof · cited by 2
- Submodule.sup_orthogonal_inf_of_hasOrthogonalProjectionproof · cited by 2