Theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField

Modification history

2026-02-06 16:14
Mathlib/AlgebraicGeometry/Fiber.lean
feat(AlgebraicGeometry): quasi-finite morphisms have finite fibers (#34898)
Added AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueFieldView on Github →