Def FractionalIdeal.extended

Modification history

2024-08-21 11:51

Mathlib/RingTheory/FractionalIdeal/Extended.lean

feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals (#14216) …

Added FractionalIdeal.extended View on Github →