Commit 2023-07-15 02:55 2f7b9952

View on Github →

feat: port AlgebraicGeometry.Morphisms.FiniteType (#5913)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

added theorem AlgebraicGeometry.LocallyOfFiniteType.affine_openCover_iff

added theorem AlgebraicGeometry.LocallyOfFiniteType.openCover_iff

added theorem AlgebraicGeometry.LocallyOfFiniteType.source_openCover_iff

added theorem AlgebraicGeometry.locallyOfFiniteTypeOfComp

added theorem AlgebraicGeometry.locallyOfFiniteType_eq

added theorem AlgebraicGeometry.locallyOfFiniteType_respectsIso

added theorem AlgebraicGeometry.locallyOfFiniteType_stableUnderComposition