Commit 2024-11-12 11:09 b762bad2

View on Github →

chore: rename LocalRing to IsLocalRing (#18774)

Estimated changes

Modified Mathlib/Algebra/CharP/LocalRing.lean

modified theorem charP_zero_or_prime_power

Modified Mathlib/Algebra/CharP/MixedCharZero.lean

modified theorem split_by_characteristic_localRing

Modified Mathlib/Algebra/Group/Units/Hom.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem IsLocalRing.PrimeSpectrum.comap_residue

added def IsLocalRing.closedPoint

added theorem IsLocalRing.closedPoint_mem_iff

added theorem IsLocalRing.closed_point_mem_iff

added theorem IsLocalRing.comap_closedPoint

added theorem IsLocalRing.isLocalHom_iff_comap_closedPoint

added theorem IsLocalRing.specializes_closedPoint

deleted theorem LocalRing.PrimeSpectrum.comap_residue

deleted def LocalRing.closedPoint

deleted theorem LocalRing.closedPoint_mem_iff

deleted theorem LocalRing.closed_point_mem_iff

deleted theorem LocalRing.comap_closedPoint

deleted theorem LocalRing.isLocalHom_iff_comap_closedPoint

deleted theorem LocalRing.specializes_closedPoint

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

Modified Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified theorem AlgebraicGeometry.Spec_closedPoint

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

modified theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/DedekindDomain/Dvr.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

modified theorem DiscreteValuationRing.irreducible_of_span_eq_maximalIdeal

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

modified theorem DiscreteValuationRing.TFAE

added theorem IsLocalRing.finrank_CotangentSpace_eq_one

added theorem IsLocalRing.finrank_CotangentSpace_eq_one_iff

deleted theorem LocalRing.finrank_CotangentSpace_eq_one

deleted theorem LocalRing.finrank_CotangentSpace_eq_one_iff

modified theorem exists_maximalIdeal_pow_eq_of_principal

modified theorem maximalIdeal_isPrincipal_of_isDedekindDomain

added theorem tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain

deleted theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain

Modified Mathlib/RingTheory/DualNumber.lean

Modified Mathlib/RingTheory/Filtration.lean

added theorem Ideal.iInf_pow_eq_bot_of_isLocalRing

deleted theorem Ideal.iInf_pow_eq_bot_of_localRing

added theorem Ideal.iInf_pow_smul_eq_bot_of_isLocalRing

deleted theorem Ideal.iInf_pow_smul_eq_bot_of_localRing

added theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing

deleted theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/Henselian.lean

modified theorem HenselianLocalRing.TFAE

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem IsLocalRing.CotangentSpace.map_eq_top_iff

added theorem IsLocalRing.CotangentSpace.span_image_eq_top_iff

added theorem IsLocalRing.finrank_cotangentSpace_eq_zero

added theorem IsLocalRing.finrank_cotangentSpace_eq_zero_iff

added theorem IsLocalRing.finrank_cotangentSpace_le_one_iff

added theorem IsLocalRing.subsingleton_cotangentSpace_iff

deleted theorem LocalRing.CotangentSpace.map_eq_top_iff

deleted theorem LocalRing.CotangentSpace.span_image_eq_top_iff

deleted theorem LocalRing.finrank_cotangentSpace_eq_zero

deleted theorem LocalRing.finrank_cotangentSpace_eq_zero_iff

deleted theorem LocalRing.finrank_cotangentSpace_le_one_iff

deleted theorem LocalRing.subsingleton_cotangentSpace_iff

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

Modified Mathlib/RingTheory/LocalRing/Basic.lean

added theorem IsLocalRing.isUnit_of_mem_nonunits_one_sub_self

added theorem IsLocalRing.isUnit_one_sub_self_of_mem_nonunits

added theorem IsLocalRing.isUnit_or_isUnit_of_isUnit_add

added theorem IsLocalRing.isUnit_or_isUnit_one_sub_self

added theorem IsLocalRing.nonunits_add

added theorem IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add

added theorem IsLocalRing.of_isUnit_or_isUnit_one_sub_self

added theorem IsLocalRing.of_nonunits_add

added theorem IsLocalRing.of_surjective'

added theorem IsLocalRing.of_unique_max_ideal

added theorem IsLocalRing.of_unique_nonzero_prime

deleted theorem LocalRing.isUnit_of_mem_nonunits_one_sub_self

deleted theorem LocalRing.isUnit_one_sub_self_of_mem_nonunits

deleted theorem LocalRing.isUnit_or_isUnit_of_isUnit_add

deleted theorem LocalRing.isUnit_or_isUnit_one_sub_self

deleted theorem LocalRing.nonunits_add

deleted theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add

deleted theorem LocalRing.of_isUnit_or_isUnit_one_sub_self

deleted theorem LocalRing.of_nonunits_add

deleted theorem LocalRing.of_surjective'

deleted theorem LocalRing.of_unique_max_ideal

deleted theorem LocalRing.of_unique_nonzero_prime

Modified Mathlib/RingTheory/LocalRing/Defs.lean

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

added theorem IsLocalRing.eq_maximalIdeal

added theorem IsLocalRing.isField_iff_maximalIdeal_eq

added theorem IsLocalRing.jacobson_eq_maximalIdeal

added theorem IsLocalRing.ker_eq_maximalIdeal

added theorem IsLocalRing.le_maximalIdeal

added theorem IsLocalRing.maximalIdeal_eq_bot

added theorem IsLocalRing.maximalIdeal_le_jacobson

added theorem IsLocalRing.maximal_ideal_unique

added theorem IsLocalRing.mem_maximalIdeal

added theorem IsLocalRing.not_mem_maximalIdeal

added theorem IsLocalRing.of_nilradical_isMaximal

deleted theorem LocalRing.eq_maximalIdeal

deleted theorem LocalRing.isField_iff_maximalIdeal_eq

deleted theorem LocalRing.jacobson_eq_maximalIdeal

deleted theorem LocalRing.ker_eq_maximalIdeal

deleted theorem LocalRing.le_maximalIdeal

deleted theorem LocalRing.maximalIdeal_eq_bot

deleted theorem LocalRing.maximalIdeal_le_jacobson

deleted theorem LocalRing.maximal_ideal_unique

deleted theorem LocalRing.mem_maximalIdeal

deleted theorem LocalRing.not_mem_maximalIdeal

deleted theorem LocalRing.of_nilradical_isMaximal

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Defs.lean

added def IsLocalRing.maximalIdeal

deleted def LocalRing.maximalIdeal

Modified Mathlib/RingTheory/LocalRing/Module.lean

added theorem IsLocalRing.map_mkQ_eq

added theorem IsLocalRing.map_mkQ_eq_top

added theorem IsLocalRing.map_tensorProduct_mk_eq_top

added theorem IsLocalRing.span_eq_top_of_tmul_eq_basis

added theorem IsLocalRing.split_injective_iff_lTensor_residueField_injective

added theorem IsLocalRing.subsingleton_tensorProduct

deleted theorem LocalRing.map_mkQ_eq

deleted theorem LocalRing.map_mkQ_eq_top

deleted theorem LocalRing.map_tensorProduct_mk_eq_top

deleted theorem LocalRing.span_eq_top_of_tmul_eq_basis

deleted theorem LocalRing.split_injective_iff_lTensor_residueField_injective

deleted theorem LocalRing.subsingleton_tensorProduct

added theorem Module.free_of_flat_of_isLocalRing

deleted theorem Module.free_of_flat_of_localRing

Modified Mathlib/RingTheory/LocalRing/Quotient.lean

added def IsLocalRing.basisQuotient

added theorem IsLocalRing.basisQuotient_apply

added theorem IsLocalRing.basisQuotient_repr

added theorem IsLocalRing.finrank_quotient_map

added theorem IsLocalRing.quotient_span_eq_top_iff_span_eq_top

deleted def LocalRing.basisQuotient

deleted theorem LocalRing.basisQuotient_apply

deleted theorem LocalRing.basisQuotient_repr

deleted theorem LocalRing.finrank_quotient_map

deleted theorem LocalRing.quotient_span_eq_top_iff_span_eq_top

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

added theorem IsLocalRing.ResidueField.algebraMap_eq

added theorem IsLocalRing.ResidueField.finite_of_finite

added def IsLocalRing.ResidueField.lift

added theorem IsLocalRing.ResidueField.lift_comp_residue

added theorem IsLocalRing.ResidueField.lift_residue_apply

added def IsLocalRing.ResidueField.map

added def IsLocalRing.ResidueField.mapAut

added theorem IsLocalRing.ResidueField.mapEquiv.symm

added def IsLocalRing.ResidueField.mapEquiv

added theorem IsLocalRing.ResidueField.mapEquiv_refl

added theorem IsLocalRing.ResidueField.mapEquiv_trans

added theorem IsLocalRing.ResidueField.map_comp

added theorem IsLocalRing.ResidueField.map_comp_residue

added theorem IsLocalRing.ResidueField.map_id

added theorem IsLocalRing.ResidueField.map_id_apply

added theorem IsLocalRing.ResidueField.map_map

added theorem IsLocalRing.ResidueField.map_residue

added theorem IsLocalRing.ResidueField.residue_smul

added theorem IsLocalRing.isLocalHom_residue

added theorem IsLocalRing.ker_residue

added theorem IsLocalRing.residue_eq_zero_iff

added theorem IsLocalRing.residue_ne_zero_iff_isUnit

added theorem IsLocalRing.residue_surjective

deleted theorem LocalRing.ResidueField.algebraMap_eq

deleted theorem LocalRing.ResidueField.finite_of_finite

deleted def LocalRing.ResidueField.lift

deleted theorem LocalRing.ResidueField.lift_comp_residue

deleted theorem LocalRing.ResidueField.lift_residue_apply

deleted def LocalRing.ResidueField.map

deleted def LocalRing.ResidueField.mapAut

deleted theorem LocalRing.ResidueField.mapEquiv.symm

deleted def LocalRing.ResidueField.mapEquiv

deleted theorem LocalRing.ResidueField.mapEquiv_refl

deleted theorem LocalRing.ResidueField.mapEquiv_trans

deleted theorem LocalRing.ResidueField.map_comp

deleted theorem LocalRing.ResidueField.map_comp_residue

deleted theorem LocalRing.ResidueField.map_id

deleted theorem LocalRing.ResidueField.map_id_apply

deleted theorem LocalRing.ResidueField.map_map

deleted theorem LocalRing.ResidueField.map_residue

deleted theorem LocalRing.ResidueField.residue_smul

deleted theorem LocalRing.isLocalHom_residue

deleted theorem LocalRing.ker_residue

deleted theorem LocalRing.residue_eq_zero_iff

deleted theorem LocalRing.residue_ne_zero_iff_isUnit

deleted theorem LocalRing.residue_surjective

Modified Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean

added def IsLocalRing.ResidueField

added def IsLocalRing.residue

deleted def LocalRing.ResidueField

deleted def LocalRing.residue

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

added theorem IsLocalRing.local_hom_TFAE

added theorem IsLocalRing.of_surjective

added theorem IsLocalRing.surjective_units_map_of_local_ringHom

deleted theorem LocalRing.local_hom_TFAE

deleted theorem LocalRing.of_surjective

deleted theorem LocalRing.surjective_units_map_of_local_ringHom

added theorem RingHom.domain_isLocalRing

deleted theorem RingHom.domain_localRing

Modified Mathlib/RingTheory/Localization/AtPrime.lean

modified theorem IsLocalization.AtPrime.comap_maximalIdeal

added theorem IsLocalization.AtPrime.isLocalRing

deleted theorem IsLocalization.AtPrime.localRing

modified theorem IsLocalization.AtPrime.mk'_mem_maximal_iff

modified theorem IsLocalization.AtPrime.to_map_mem_maximal_iff

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

modified theorem PowerSeries.maximalIdeal_eq_span_X

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

added theorem IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal

added theorem IsLocalRing.isRegular_of_perm

added theorem IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal

deleted theorem LocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal

deleted theorem LocalRing.isRegular_of_perm

deleted theorem LocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal

Modified Mathlib/RingTheory/SurjectiveOnStalks.lean

modified theorem RingHom.surjectiveOnStalks_iff_of_isLocalHom

Modified Mathlib/RingTheory/Trace/Quotient.lean

modified theorem Algebra.trace_quotient_mk

Modified Mathlib/RingTheory/Unramified/Field.lean

added theorem Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing

deleted theorem Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_localRing

added theorem Algebra.FormallyUnramified.isField_of_isAlgClosed_of_isLocalRing

deleted theorem Algebra.FormallyUnramified.isField_of_isAlgClosed_of_localRing

Modified Mathlib/RingTheory/Valuation/RamificationGroup.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

modified theorem ValuationRing.iff_local_bezout_domain

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

modified theorem ValuationSubring.coe_mem_nonunits_iff

modified theorem ValuationSubring.image_maximalIdeal

modified theorem ValuationSubring.principalUnitGroup_symm_apply

modified def ValuationSubring.unitGroupToResidueFieldUnits

modified theorem ValuationSubring.valuation_lt_one_iff

Modified Mathlib/Topology/Algebra/Valued/ValuedField.lean

modified def Valued.ResidueField

modified def Valued.maximalIdeal

Modified docs/overview.yaml

Modified scripts/no_lints_prime_decls.txt