Theorem AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp

Modification history

2025-09-19 16:11

Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean

refactor(AlgebraicGeometry): rename fields of `Scheme.Cover` to match `ZeroHypercover` (#29803) …

Modified AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp View on Github →

2025-07-23 10:07

Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean

feat(AlgebraicGeometry): source-local closure of a morphism property (#26723) …

Added AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp View on Github →