Theorem AlgebraicGeometry.isInitial_iff_isEmpty

Modification history

2026-01-16 12:21
Mathlib/AlgebraicGeometry/Limits.lean
feat(AlgebraicGeometry): `Scheme` has disjoint coproducts (#34014) …
Added AlgebraicGeometry.isInitial_iff_isEmptyView on Github →