Theorems · Theorem · commutative algebra
Ideal.exact_mulQuot_quotOfMul
∀ {R : Type u_1} [inst : CommRing R] {a : R} (I : Ideal R), Function.Exact ⇑(Ideal.mulQuot a I) ⇑(Ideal.quotOfMul a I)The sequence R ⧸ I →ₗ[R] R ⧸ (a • I) →ₗ[R] R ⧸ (Ideal.span {a}) given by multiplication
by a then quotienting by the ideal generated by a is exact.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites36
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapstatement · cited by 10,215
- Top.topproof · cited by 9,680
- Idealstatement and proof · cited by 4,748
- HasQuotient.Quotientstatement · cited by 2,301
- LinearMap.compproof · cited by 1,642
- Submodule.spanproof · cited by 1,504
- Ideal.spanstatement and proof · cited by 948
- LinearMap.rangeproof · cited by 893
Cited by1
Results whose statement or proof uses this declaration.
- Ring.ord_mulproof · cited by 3