Theorem Ideal.count_associates_eq'

Modification history

2026-02-27 09:51
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat: classical "decidability" instances on sets and ideals (#33757) …
Modified Ideal.count_associates_eq'View on Github →
2025-06-30 09:49
Mathlib/RingTheory/DedekindDomain/Ideal.lean
feat: Ideal.count_associates_eq (#23955) …
Added Ideal.count_associates_eq'View on Github →