Theorem IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv

Modification history

2024-11-13 14:41
Mathlib/RingTheory/Localization/FractionRing.lean
feat(RingTheory/Localization/*): add `IsLocalization.algEquivOfAlgEquiv` and other results (#18661) …
Added IsFractionRing.restrictScalars_fieldEquivOfAlgEquivView on Github →