Theorem RatFunc.liftRingHom_ofFractionRing_algebraMap

Modification history

2025-12-15 10:15
Mathlib/FieldTheory/RatFunc/Basic.lean
feat(RingTheory): residue field of `I[X]` (#32809)
Added RatFunc.liftRingHom_ofFractionRing_algebraMapView on Github →