mathlib
3d97cfb1 - feat(ring_theory/ideal,dedekind_domain): lemmas on `I ≤ I^e` and `I < I^e` (#12185)

Commit

3 years ago

feat(ring_theory/ideal,dedekind_domain): lemmas on `I ≤ I^e` and `I < I^e` (#12185)

Author

Vierkantor

Parents