Commit 2024-05-29 09:23 f400f9b2

View on Github →

chore(RingTheory/GradedAlgebra/HomogeneousLocalization) New simp lemmas (#13037) Also used the new simp lemmas to golf AlgebraicGeometry/ProjectiveSpectrum/*

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.eventually_exists

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.eventually_mem_ideal

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff_exists

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier

modified theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen

modified theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

added theorem AlgebraicGeometry.Proj.add_apply

added theorem AlgebraicGeometry.Proj.ext

added theorem AlgebraicGeometry.Proj.mul_apply

added theorem AlgebraicGeometry.Proj.one_apply

added theorem AlgebraicGeometry.Proj.pow_apply

modified theorem AlgebraicGeometry.Proj.res_apply

deleted theorem AlgebraicGeometry.Proj.stalkIso'_symm_mk''

added theorem AlgebraicGeometry.Proj.stalkIso'_symm_mk

added theorem AlgebraicGeometry.Proj.sub_apply

added theorem AlgebraicGeometry.Proj.zero_apply

deleted theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.addMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem'

deleted theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem'

deleted theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.negMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem'

deleted theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.oneMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem'

deleted theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zeroMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem'

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

deleted theorem HomogeneousLocalization.add_val

deleted theorem HomogeneousLocalization.intCast_val

modified theorem HomogeneousLocalization.isUnit_iff_isUnit_val

added theorem HomogeneousLocalization.mk_add

added theorem HomogeneousLocalization.mk_eq_zero_of_den

added theorem HomogeneousLocalization.mk_eq_zero_of_num

added theorem HomogeneousLocalization.mk_mul

added theorem HomogeneousLocalization.mk_neg

added theorem HomogeneousLocalization.mk_one

added theorem HomogeneousLocalization.mk_pow

added theorem HomogeneousLocalization.mk_smul

added theorem HomogeneousLocalization.mk_surjective

added theorem HomogeneousLocalization.mk_zero

deleted theorem HomogeneousLocalization.mul_val

deleted theorem HomogeneousLocalization.natCast_val

deleted theorem HomogeneousLocalization.neg_val

deleted theorem HomogeneousLocalization.one_val

deleted theorem HomogeneousLocalization.pow_val

deleted theorem HomogeneousLocalization.smul_val

deleted theorem HomogeneousLocalization.sub_val

added theorem HomogeneousLocalization.subsingleton

added theorem HomogeneousLocalization.val_add

added theorem HomogeneousLocalization.val_intCast

deleted theorem HomogeneousLocalization.val_mk''

added theorem HomogeneousLocalization.val_mk

added theorem HomogeneousLocalization.val_mul

added theorem HomogeneousLocalization.val_natCast

added theorem HomogeneousLocalization.val_neg

added theorem HomogeneousLocalization.val_one

added theorem HomogeneousLocalization.val_pow

added theorem HomogeneousLocalization.val_smul

added theorem HomogeneousLocalization.val_sub

added theorem HomogeneousLocalization.val_zero

deleted theorem HomogeneousLocalization.zero_val