Theorems · Theorem · commutative algebra
isSMulRegular_quotient_iff_mem_of_smul_mem
∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
(r : R), IsSMulRegular (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N → x ∈ N- Defined in
- Mathlib.RingTheory.Regular.IsSMulRegular
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- 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
- HasQuotient.Quotientstatement · cited by 2,301
- Submodule.mkQproof · cited by 232
- Function.Surjective.forallproof · cited by 214
- IsSMulRegularstatement · cited by 128
- Submodule.mkQ_surjectiveproof · cited by 48
- isSMulRegular_iff_right_eq_zero_of_smulproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- isSMulRegular_on_quot_iff_lsmul_comap_leproof · cited by 3
- mem_of_isSMulRegular_quotient_of_smul_memproof · cited by 0