Theorem IsFractionRing.of_algEquiv

Modification history

2026-04-13 15:12
Mathlib/RingTheory/Localization/FractionRing.lean
feat(FieldTheory/IntermediateField): define the image of an intermediate field in a larger extension (#36772) …
Added IsFractionRing.of_algEquivView on Github →