Commit 2026-06-25 05:38 2da22206

View on Github →

chore(AlgebraicGeometry/AffineScheme): golf using simp (#40991) As recommended in the style guide. Extracted from https://github.com/leanprover-community/mathlib4/pull/40793.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

deleted def AlgebraicGeometry.SpecMapRestrictBasicOpenIso

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMap