Mathlib v3 is deprecated. Go to Mathlib v4

Def algebraic_geometry.Spec_Γ_identity

Modification history

2022-01-14 08:37
src/algebraic_geometry/Spec.lean
feat(algebraic_geometry): lemmas about basic opens in schemes (#11393)
Modified algebraic_geometry.Spec_Γ_identityView on Github →
2021-10-01 12:27
src/algebraic_geometry/Spec.lean
feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 (#9416) …
Added algebraic_geometry.Spec_Γ_identityView on Github →