Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.degree_zero_part.coe_sum

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.coe_sumView on Github →
2022-09-26 09:37
src/algebraic_geometry/projective_spectrum/scheme.lean
feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259) …
Added algebraic_geometry.degree_zero_part.coe_sumView on Github →