Theorem AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed

Modification history

2026-06-18 11:17
Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean
feat(AlgebraicGeometry): points of the small étale site (#35136) …
Added AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosedView on Github →