Theorem AlgebraicGeometry.of_affine_open_cover

Modification history

2024-06-25 05:48

Mathlib/AlgebraicGeometry/AffineScheme.lean

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

Modified AlgebraicGeometry.of_affine_open_cover View on Github →

2023-06-29 07:18

Mathlib/AlgebraicGeometry/AffineScheme.lean

feat: port AlgebraicGeometry.AffineScheme (#5394)

Added AlgebraicGeometry.of_affine_open_cover View on Github →