Theorems · Theorem · commutative algebra
Ideal.LiesOver.of_eq_comap
∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} {C : Type u_4} [inst_1 : Semiring B] [inst_2 : Semiring C]
[inst_3 : Algebra A B] [inst_4 : Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] {F : Type u_6}
[inst_6 : FunLike F B C] [inst_7 : AlgHomClass F A B C] (f : F), P = Ideal.comap f Q → P.LiesOver p- Defined in
- Mathlib.RingTheory.Ideal.Over
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 23 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
- Idealstatement and proof · cited by 4,748
- FunLikestatement and proof · cited by 2,560
- Ideal.comapstatement and proof · cited by 443
- Ideal.LiesOverstatement and proof · cited by 272
- Ideal.underproof · cited by 170
- AlgHom.comp_algebraMapproof · cited by 63
- Ideal.over_defproof · cited by 60
- AlgHomClassstatement and proof · cited by 50
- AlgHomClass.toAlgHomproof · cited by 14
Cited by1
Results whose statement or proof uses this declaration.
- Ideal.LiesOver.of_eq_map_equivproof · cited by 0