Commit 2025-06-30 09:49 d8810ed3

View on Github →

feat: Ideal.count_associates_eq (#23955) Add variant of UniqueFactorizationMonoid.count_normalizedFactors_eq for associated Ideals. This is convenient when you need to talk about an element as a₀ = x ^ n * a. Note the file is slightly over the 1500 lines limit, I hope that is ok.

Estimated changes