Theorems · Theorem · commutative algebra
IsLocalization.AtPrime.equivQuotMaximalIdealPow_symm_apply_mk_mul
∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
[inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (n : ℕ) (x : R)
(s : ↥p.primeCompl),
(IsLocalization.AtPrime.equivQuotMaximalIdealPow p Rₚ n).symm
((Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ ^ n)) (IsLocalization.mk' Rₚ x s)) *
(Ideal.Quotient.mk (p ^ n)) ↑s =
(Ideal.Quotient.mk (p ^ n)) x- Cited by
- 0 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Idealstatement and proof · cited by 4,748
- mul_oneproof · cited by 3,885
- Submonoidstatement · cited by 3,086
- HasQuotient.Quotientstatement and proof · cited by 2,301
- Units.valproof · cited by 1,966
- AlgEquivstatement · cited by 1,681
- mul_assocproof · cited by 1,667
- RingHomClass.toRingHomproof · cited by 746
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.