Theorem AlgHom.liftOfSurjective_apply

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Ideal/Quotient/Operations.lean
feat(RingTheory): residue field of `I[X]` (#32809)
Added AlgHom.liftOfSurjective_applyView on Github →