Commit 2025-02-17 13:55 fcc2f28d

View on Github →

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

Estimated changes

modified theorem FractionalIdeal.count_mul'