Theorem Ideal.finprod_heightOneSpectrum_factorization_coeIdeal

Modification history

2026-11-10 17:26
Mathlib/RingTheory/DedekindDomain/Factorization.lean
chore: correct naming of coercion lemmas about coeIdeal (#45832) …
Added Ideal.finprod_heightOneSpectrum_factorization_coeIdealView on Github →