Theorem AlgebraicGeometry.locallyOfFiniteTypeOfComp

Modification history

2024-06-25 05:48

Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

refactor(AlgebraicGeometry): Use `Scheme.Hom.app` as simp normal form (#14031)

Deleted AlgebraicGeometry.locallyOfFiniteTypeOfComp View on Github →

2023-07-15 02:55

Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

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

Added AlgebraicGeometry.locallyOfFiniteTypeOfComp View on Github →