Mathlib Changelog
v3
Changelog
About
Github
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