Mathlib Changelog
v4
Changelog
About
Github
Theorem
FractionalIdeal.count_coeIdeal_nonneg
Modification history
2026-11-10 17:26
Mathlib/RingTheory/DedekindDomain/Factorization.lean
chore: correct naming of coercion lemmas about coeIdeal (#45832) …
Added
FractionalIdeal.count_coeIdeal_nonneg
View on Github →