Theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_eq

Modification history

2024-05-18 18:12

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

chore(AlgebraicGeometry/ProjectiveSpectrum/Scheme): Tidy & golf (#12981)

Deleted AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_eq View on Github →

2024-04-04 23:53

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): `fromSpec` is a continuous function so that we have `Spec A^0_f = Proj | D(f)` as topological spaces (#9629)

Added AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_eq View on Github →