Theorem IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq

Modification history

2025-01-10 18:59
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) …
Modified IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eqView on Github →
2024-11-21 15:34
Mathlib/FieldTheory/Adjoin.lean
feat: add `IsFractionRing.lift[AlgHom]_fieldRange[_eq_of_range_eq]` (#19286) …
Added IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eqView on Github →