Def IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq

Modification history

2026-03-17 12:17
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(DedekindDomain/Factorization): add `iInf` version of `finprod_heightOneSpectrum_factorization` (#35539) …
Added IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEqView on Github →