Theorems · Theorem · commutative algebra
Submodule.coe_mem
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
(x : ↥p), ↑x ∈ p- Defined in
- Mathlib.Algebra.Module.Submodule.Defs
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
- Assumes
- SemiringAddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Submodulestatement and proof · cited by 7,192
Cited by24
Results whose statement or proof uses this declaration.
- Submodule.eq_starProjection_of_mem_of_inner_eq_zeroproof · cited by 6
- ZLattice.rankproof · cited by 5
- LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZeroproof · cited by 5
- Submodule.inner_orthogonalProjectionOnto_eq_of_mem_rightproof · cited by 5
- Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInfproof · cited by 5
- IsSl2Triple.h_eq_corootproof · cited by 4
- Ideal.map_includeRight_eqproof · cited by 3
- ZLattice.covolume_div_covolume_eq_relIndexproof · cited by 2
- Submodule.mem_iSup_finset_iff_exists_sumproof · cited by 2
- Module.Basis.sumQuot_repr_inrproof · cited by 2
- Submodule.restrictScalars_image_smul_eqproof · cited by 2
- LinearMap.det_eq_det_mul_detproof · cited by 1