Commit 2024-03-01 17:22 c26b7f13

View on Github →

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

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecFromSpec

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective