Theorems · Definition · commutative algebra
QuotSMulTop
{R : Type u_2} → [inst : CommRing R] → R → (M : Type u_1) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_1An abbreviation for M⧸rM that keeps us from having to write
(⊤ : Submodule R M) over and over to satisfy the typechecker.
- Defined in
- Mathlib.RingTheory.QuotSMulTop
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingAddCommGroupModule
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
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- Top.topproof · cited by 9,680
- HasQuotient.Quotientproof · cited by 2,301
Cited by63
Results whose statement or proof uses this declaration.
- QuotSMulTop.mapstatement · cited by 13
- Submodule.quotOfListConsSMulTopEquivQuotSMulTopInnerstatement · cited by 7
- RingTheory.Sequence.isWeaklyRegular_cons_iffstatement and proof · cited by 6
- RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChangeproof · cited by 3
- RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularstatement and proof · cited by 3
- RingTheory.Sequence.isRegular_cons_iffstatement and proof · cited by 2
- Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobsonstatement and proof · cited by 2
- Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobsonstatement · cited by 2
- Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobsonstatement · cited by 2
- RingTheory.Sequence.isWeaklyRegular_cons_iff'statement and proof · cited by 2
- Module.support_quotSMulTopstatement · cited by 2
- ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobsonstatement · cited by 2