Theorems · Theorem · commutative algebra
Ideal.LiesOver.trans
∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
[inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B)
(p : Ideal A) [𝔓.LiesOver P] [P.LiesOver p], 𝔓.LiesOver p- Defined in
- Mathlib.RingTheory.Ideal.Over
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Idealstatement and proof · cited by 4,748
- IsScalarTowerstatement and proof · cited by 3,896
- Ideal.LiesOverstatement and proof · cited by 272
- Ideal.underproof · cited by 170
- Ideal.over_defproof · cited by 60
- Ideal.under_underproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- Ideal.absNorm_relNormproof · cited by 2
- IsUnramifiedAt.of_liesOver_of_ne_botproof · cited by 1
- Ideal.ramificationIdxIn_mul_ramificationIdxInproof · cited by 1
- Ideal.relNorm_eq_pow_of_isMaximalproof · cited by 1
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eqproof · cited by 1
- Ideal.inertiaDeg'_le_inertiaDeg'proof · cited by 1
- Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOverproof · cited by 1
- Algebra.WeaklyQuasiFiniteAt.finite_residueFieldproof · cited by 1
- IsLocalization.AtPrime.liesOver_comap_of_liesOverproof · cited by 0
- Ideal.ncard_primesOver_mul_ncard_primesOverproof · cited by 0
- Ideal.inertiaDegIn_mul_inertiaDegInproof · cited by 0