Theorem IsFractionRing.fieldEquivOfAlgEquivHom_apply

Modification history

2024-10-31 21:40
Mathlib/RingTheory/Localization/FractionRing.lean
feat(RingTheory/Localization/FractionRing): Lifting `AlgEquiv`s to the field of fractions (#17753) …
Added IsFractionRing.fieldEquivOfAlgEquivHom_applyView on Github →