Commit 2024-10-31 21:40 c3345c14

View on Github →

feat(RingTheory/Localization/FractionRing): Lifting AlgEquivs to the field of fractions (#17753) This PR adds some API for lifting AlgEquivs to the field of fractions.

Estimated changes

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem IsFractionRing.fieldEquivOfAlgEquivHom_apply

added theorem IsFractionRing.fieldEquivOfAlgEquiv_algebraMap

added theorem IsFractionRing.fieldEquivOfAlgEquiv_refl

added theorem IsFractionRing.fieldEquivOfAlgEquiv_trans

added theorem IsFractionRing.fieldEquivOfRingEquiv_algebraMap

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean