Theorems · Theorem · commutative algebra
Ideal.map_ne_bot_of_ne_bot
∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] [FaithfulSMul R S]
{I : Ideal R}, I ≠ ⊥ → Ideal.map (algebraMap R S) I ≠ ⊥- Defined in
- Mathlib.RingTheory.Ideal.Maps
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- Idealstatement and proof · cited by 4,748
- Bot.botstatement and proof · cited by 4,720
- Algebra.algebraMapstatement · cited by 4,706
- Ideal.mapstatement · cited by 692
- FaithfulSMulstatement and proof · cited by 340
- FaithfulSMul.algebraMap_injectiveproof · cited by 198
- Function.mtproof · cited by 27
- Ideal.map_eq_bot_iff_of_injectiveproof · cited by 14
Cited by7
Results whose statement or proof uses this declaration.
- Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOverproof · cited by 6
- IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_oneproof · cited by 4
- Ideal.mem_primesOver_iff_mem_normalizedFactorsproof · cited by 2
- Ideal.map_algebraMap_eq_finsetProd_powproof · cited by 2
- Ideal.ramificationIdx'_eq_ramificationIdxproof · cited by 1
- Ideal.ramificationIdx'_algebra_tower'proof · cited by 1