Theorem FractionalIdeal.mem_extended_iff

Modification history

2025-09-26 06:18

Mathlib/RingTheory/FractionalIdeal/Extended.lean

chore(RingTheory): golf entire `coeff_opRingEquiv` and `comp_assoc` using `rfl` (#28571)

Modified FractionalIdeal.mem_extended_iff View on Github →

2024-08-21 11:51

Mathlib/RingTheory/FractionalIdeal/Extended.lean

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

Added FractionalIdeal.mem_extended_iff View on Github →