Commit 2025-03-31 08:28 0e7ba015

View on Github →

chore(AlgebraicGeometry/AffineScheme): rename isAffine_of_isIso to IsAffine.of_isIso (#23475) This is useful for anonymous dot notation. From Toric

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffine.of_isIso

deleted theorem AlgebraicGeometry.isAffine_of_isIso

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean