Theorem AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne

Modification history

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