Theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_eq_span

Modification history

2024-05-18 18:12

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

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

Deleted AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_eq_span 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.ToSpec.carrier_eq_span View on Github →