Theorem FractionalIdeal.isLocalizationMap_coeIdealHom

Modification history

2026-10-18 08:25
Mathlib/RingTheory/FractionalIdeal/Operations.lean
feat(RingTheory/FractionalIdeal): add HasUniqueRoots instance (#40636) …
Added FractionalIdeal.isLocalizationMap_coeIdealHomView on Github →