Theorem Ideal.map_algebraMap_eq_finset_prod_pow

Modification history

2026-04-26 16:26
Mathlib/RingTheory/DedekindDomain/Factorization.lean
chore: camel-case `finset_sum` in lemma names (#37793) …
Deleted Ideal.map_algebraMap_eq_finset_prod_powView on Github →
2025-09-22 16:24
Mathlib/RingTheory/DedekindDomain/Factorization.lean
feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension (#27105) …
Added Ideal.map_algebraMap_eq_finset_prod_powView on Github →