Theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ

Modification history

2024-10-10 07:55
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
refactor(Topology/Sheaves): Unbundle `germ`. (#15314)
Modified AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germView on Github →
2024-06-11 06:47
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): morphism of locally ringed space $\mathrm{Proj}|_{D(f)} -> \mathrm{Spec} A^0_f$ (#13689) …
Added AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germView on Github →