Def AlgebraicGeometry.Scheme.isoSpec

Modification history

2024-06-25 05:48

Mathlib/AlgebraicGeometry/AffineScheme.lean

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

Modified AlgebraicGeometry.Scheme.isoSpec View on Github →

2023-06-29 07:18

Mathlib/AlgebraicGeometry/AffineScheme.lean

feat: port AlgebraicGeometry.AffineScheme (#5394)

Added AlgebraicGeometry.Scheme.isoSpec View on Github →