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 →