Def algebraic_geometry.degree_zero_part.deg

Modification history

2022-10-05 18:04
src/algebraic_geometry/projective_spectrum/scheme.lean
refactor(algebraic_geometry/projective_spectrum/scheme): use homogenous localization API (#16693)
Deleted algebraic_geometry.degree_zero_part.degView on Github →
2022-07-11 14:26
src/algebraic_geometry/projective_spectrum/scheme.lean
feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397) …
Modified algebraic_geometry.degree_zero_part.degView on Github →
2022-04-21 12:09
src/algebraic_geometry/projective_spectrum/scheme.lean
feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398) …
Added algebraic_geometry.degree_zero_part.degView on Github →