Theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecFromSpec

Modification history

2024-03-01 17:22

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): `fromSpec` and `toSpec` compose to identity (#9618)

Deleted AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecFromSpec View on Github →

2024-02-27 13:37

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): `toSpec` and `fromSpec` compose to identity (#9601)

Added AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecFromSpec View on Github →