Theorems · Theorem · commutative algebra

Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P Q : Ideal S}
  [P.IsPrime] [inst_4 : Q.IsPrime],
  P ≤ Q → Ideal.under R P = Ideal.under R Q → ∀ [Algebra.WeaklyQuasiFiniteAt R Q], P = Q

Use Algebra.QuasiFiniteAt.eq_of_le_of_under_eq instead for Algebra.QuasiFiniteAt R p.

Defined in

Mathlib.RingTheory.QuasiFinite.Weakly

Cited by

0 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeIdeal.IsPrimeAlgebra.WeaklyQuasiFiniteAt