Commit 2025-10-06 14:26 c61c9d2c

View on Github →

chore(AlgebraicGeometry/Sites): golf entire pretopology_eq_inf using rfl (#30243)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/Pretopology.lean

modified theorem AlgebraicGeometry.Scheme.pretopology_eq_inf