Theorem FractionalIdeal.den_mem_inv

Modification history

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