Commit 2024-05-18 18:12 db0686ca

View on Github →

chore(AlgebraicGeometry/ProjectiveSpectrum/Scheme): Tidy & golf (#12981)

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator'

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.eventually_exists

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.eventually_mem_ideal

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_eq_span

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_ne_top

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.disjoint

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff_exists

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_eq

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_eq

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

deleted theorem AlgebraicGeometry.HomogeneousLocalization.mem_basicOpen

added theorem AlgebraicGeometry.Proj.res_apply

added theorem AlgebraicGeometry.Proj.stalkIso'_germ'

added theorem AlgebraicGeometry.Proj.stalkIso'_germ

added theorem AlgebraicGeometry.Proj.stalkIso'_symm_mk''

modified def AlgebraicGeometry.homogeneousLocalizationToStalk

added theorem AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom

added theorem AlgebraicGeometry.mem_basicOpen_den

deleted theorem AlgebraicGeometry.res_apply

added theorem AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean

added theorem HomogeneousIdeal.ext'

added theorem Ideal.IsHomogeneous.mem_iff

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

added theorem HomogeneousLocalization.Away.eventually_smul_mem

added theorem HomogeneousLocalization.algebraMap_apply

added theorem HomogeneousLocalization.den_smul_val

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

deleted theorem Ideal.mem_radical_of_pow_mem

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.disjoint_powers_iff_not_mem

added theorem Ideal.mem_radical_of_pow_mem

Modified Mathlib/RingTheory/Jacobson.lean

deleted theorem Ideal.disjoint_powers_iff_not_mem