Theorem FractionalIdeal.count_maximal

Modification history

2025-02-17 13:55

Mathlib/RingTheory/DedekindDomain/Factorization.lean

chore(RingTheory/DedekindDomain/Factorisation.lean): remove bare open… (#21978) …

Modified FractionalIdeal.count_maximal View on Github →

2024-05-13 15:49

Mathlib/RingTheory/DedekindDomain/Factorization.lean

feat(RingTheory.DedekindDomain.Factorization): add factorization of fractional ideals (#7778) …

Added FractionalIdeal.count_maximal View on Github →