Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 18:04 735ce9d9

View on Github →

refactor(algebraic_geometry/projective_spectrum/scheme): use homogenous localization API (#16693)

Estimated changes

Modified src/algebraic_geometry/projective_spectrum/scheme.lean

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.add_mem

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.homogeneous

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.ne_top

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.prime

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.denom_not_mem

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.relevant

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.smul_mem

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.zero_mem

modified def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff'

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff

modified def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.to_fun

modified def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier.clear_denominator'

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier_iff

modified theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.preimage_eq

modified def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.to_fun

modified def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec

deleted theorem algebraic_geometry.degree_zero_part.coe_mul

deleted theorem algebraic_geometry.degree_zero_part.coe_one

deleted theorem algebraic_geometry.degree_zero_part.coe_sum

deleted def algebraic_geometry.degree_zero_part.deg

deleted theorem algebraic_geometry.degree_zero_part.eq

deleted def algebraic_geometry.degree_zero_part.num

deleted theorem algebraic_geometry.degree_zero_part.num_mem

deleted def algebraic_geometry.degree_zero_part