Theorem FractionalIdeal.le_one_of_extendedHom_le_one

Modification history

2026-04-16 14:44
Mathlib/RingTheory/FractionalIdeal/Extended.lean
chore: rename FractionalIdeal.extendedHom (#38116) …
Added FractionalIdeal.le_one_of_extendedHom_le_oneView on Github →