Theorem AlgebraicGeometry.ΓSpec.adjunction_homEquiv

Modification history

2024-10-16 11:05
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
refactor(AlgebraicGeometry): Make `Scheme.Hom` a structure. (#15093) …
Deleted AlgebraicGeometry.ΓSpec.adjunction_homEquivView on Github →
2023-06-22 15:02
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
feat: port AlgebraicGeometry.GammaSpecAdjunction (#5079)
Added AlgebraicGeometry.ΓSpec.adjunction_homEquivView on Github →