Theorem AlgebraicGeometry.reduce_to_affine_nbhd

Modification history

2024-06-25 05:48

Mathlib/AlgebraicGeometry/Properties.lean

refactor(AlgebraicGeometry): Use `Scheme.Hom.app` as simp normal form (#14031)

Modified AlgebraicGeometry.reduce_to_affine_nbhd View on Github →

2023-06-29 14:20

Mathlib/AlgebraicGeometry/Properties.lean

feat: port AlgebraicGeometry.Properties (#5585)

Added AlgebraicGeometry.reduce_to_affine_nbhd View on Github →