Theorem AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMap

Modification history

2026-06-25 05:38
Mathlib/AlgebraicGeometry/Restrict.lean
chore(AlgebraicGeometry/AffineScheme): golf using `simp` (#40991) …
Added AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMapView on Github →