Theorems · Inductive type · commutative algebra
Ideal.LiesOver
{A : Type u_2} →
[inst : CommSemiring A] → {B : Type u_3} → [inst_1 : Semiring B] → [Algebra A B] → Ideal B → Ideal A → PropP lies over p if p is the preimage of P by the algebraMap.
- Defined in
- Mathlib.RingTheory.Ideal.Over
- Cited by
- 272 results in Mathlib
- Foundations
- Depth 15 from the axioms, rests on 130 definitions · uses no axioms
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- Algebrastatement · cited by 11,388
- CommSemiringstatement · cited by 10,911
- Idealstatement · cited by 4,748
Cited by300
Results whose statement or proof uses this declaration.
- Ideal.primesOverproof · cited by 84
- Ideal.over_defstatement and proof · cited by 60
- Localization.AtPrime.algebraOfLiesOverstatement and proof · cited by 30
- Localization.AtPrime.IsLiesOverAlgebrastatement · cited by 23
- Ideal.LiesOver.overstatement and proof · cited by 23
- Ideal.ramificationIdxInproof · cited by 18
- Ideal.inertiaDegInproof · cited by 18
- Ideal.LiesOver.transstatement and proof · cited by 12
- Ideal.inertiaDeg'_algebraMapstatement and proof · cited by 11
- Ideal.inertiaDegIn_eq_inertiaDegstatement and proof · cited by 11
- Ideal.Quotient.stabilizerHomstatement and proof · cited by 10
- Ideal.ramificationIdxIn_eq_ramificationIdxstatement and proof · cited by 10
Showing the 200 most cited of 300.