Theorem FractionalIdeal.divMod_zero_left

Modification history

2025-06-14 13:55

Mathlib/RingTheory/DedekindDomain/Factorization.lean

feat(NumberTheory): discriminant is norm of different (#25792)

Added FractionalIdeal.divMod_zero_left View on Github →