Theorem Ideal.Fiber.lift_residueField_surjective

Modification history

2026-02-09 11:07
Mathlib/RingTheory/QuasiFinite/Basic.lean
feat(RingTheory): local structure for finite unramified algebras (#34928)
Added Ideal.Fiber.lift_residueField_surjectiveView on Github →