Def FractionalIdeal.map

Modification history

2024-01-19 16:41

Mathlib/RingTheory/FractionalIdeal/Basic.lean

chore: Split `RingTheory.FractionalIdeal.Basic` (#9854) …

Modified FractionalIdeal.map View on Github →

2023-05-23 18:30

Mathlib/RingTheory/FractionalIdeal.lean

feat: port RingTheory.FractionalIdeal (#4243)

Added FractionalIdeal.map View on Github →