Theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι

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_fiberι View on Github →