Theorems · Theorem · commutative algebra
Ideal.map_jacobson_of_surjective
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {I : Ideal R} {f : R →+* S},
Function.Surjective ⇑f → RingHom.ker f ≤ I → Ideal.map f I.jacobson = (Ideal.map f I).jacobson- Defined in
- Mathlib.RingTheory.Jacobson.Ideal
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
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
- RingHomstatement and proof · cited by 10,189
- Top.topproof · cited by 9,680
- Ringstatement and proof · cited by 7,463
- Set.ofPredproof · cited by 6,101
- Set.imageproof · cited by 5,609
- Idealstatement and proof · cited by 4,748
- le_antisymmproof · cited by 2,068
- le_transproof · cited by 985
- Ideal.mapstatement and proof · cited by 692
- Ideal.IsMaximalproof · cited by 452
- Ideal.comapproof · cited by 443
Cited by4
Results whose statement or proof uses this declaration.
- Ideal.jacobson_eq_iff_jacobson_quotient_eq_botproof · cited by 2
- Ideal.map_jacobson_of_bijectiveproof · cited by 1
- Polynomial.isJacobsonRing_polynomial_of_isJacobsonRingproof · cited by 1
- Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_botproof · cited by 0