Theorem FractionalIdeal.num_le_mul_inv

Modification history

2025-07-31 15:44
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
chore: split long file `DedekindDomain/Ideal.lean` (#27676) …
Modified FractionalIdeal.num_le_mul_invView on Github →
2024-06-30 19:02
Mathlib/RingTheory/DedekindDomain/Ideal.lean
feat: simple lemmas about fractional ideals (#14099) …
Added FractionalIdeal.num_le_mul_invView on Github →