Commit 2024-10-31 23:26 2e82aa21

View on Github →

chore(RingTheory/Jacobson): Rename Ideal.IsJacobson to IsJacobsonRing. (#18271)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

deleted theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobson

added theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing

deleted theorem PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobson

added theorem PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing

Modified Mathlib/RingTheory/Jacobson.lean

deleted theorem Ideal.IsJacobson.out

deleted theorem Ideal.MvPolynomial.comp_C_integral_of_surjective_of_jacobson

deleted theorem Ideal.MvPolynomial.isJacobson_MvPolynomial_fin

deleted theorem Ideal.MvPolynomial.quotient_mk_comp_C_isIntegral_of_jacobson

deleted theorem Ideal.Polynomial.Subring.mem_closure_image_of

deleted theorem Ideal.Polynomial.comp_C_integral_of_surjective_of_jacobson

deleted theorem Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient

deleted theorem Ideal.Polynomial.isJacobson_polynomial_iff_isJacobson

deleted theorem Ideal.Polynomial.isJacobson_polynomial_of_isJacobson

deleted theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson'

deleted theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson

deleted theorem Ideal.Polynomial.isMaximal_comap_C_of_isMaximal

deleted theorem Ideal.Polynomial.jacobson_bot_of_integral_localization

deleted theorem Ideal.Polynomial.mem_closure_X_union_C

deleted theorem Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson

deleted theorem Ideal.isJacobson_iff

deleted theorem Ideal.isJacobson_iff_prime_eq

deleted theorem Ideal.isJacobson_iff_sInf_maximal'

deleted theorem Ideal.isJacobson_iff_sInf_maximal

deleted theorem Ideal.isJacobson_iso

deleted theorem Ideal.isJacobson_localization

deleted theorem Ideal.isJacobson_of_isIntegral'

deleted theorem Ideal.isJacobson_of_isIntegral

deleted theorem Ideal.isJacobson_of_surjective

deleted theorem Ideal.isMaximal_iff_isMaximal_disjoint

deleted theorem Ideal.isMaximal_of_isMaximal_disjoint

deleted def Ideal.orderIsoOfMaximal

modified theorem Ideal.radical_eq_jacobson

added theorem IsJacobsonRing.out

added theorem IsLocalization.isMaximal_iff_isMaximal_disjoint

added theorem IsLocalization.isMaximal_of_isMaximal_disjoint

added def IsLocalization.orderIsoOfMaximal

added theorem MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing

added theorem MvPolynomial.isJacobsonRing_MvPolynomial_fin

added theorem MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing

added theorem Polynomial.Subring.mem_closure_image_of

added theorem Polynomial.comp_C_integral_of_surjective_of_isJacobsonRing

added theorem Polynomial.isIntegral_isLocalization_polynomial_quotient

added theorem Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing

added theorem Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing

added theorem Polynomial.isMaximal_comap_C_of_isJacobsonRing

added theorem Polynomial.isMaximal_comap_C_of_isMaximal

added theorem Polynomial.jacobson_bot_of_integral_localization

added theorem Polynomial.mem_closure_X_union_C

added theorem Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing

added theorem isJacobsonRing_iff

added theorem isJacobsonRing_iff_prime_eq

added theorem isJacobsonRing_iff_sInf_maximal'

added theorem isJacobsonRing_iff_sInf_maximal

added theorem isJacobsonRing_iso

added theorem isJacobsonRing_localization

added theorem isJacobsonRing_of_isIntegral'

added theorem isJacobsonRing_of_isIntegral

added theorem isJacobsonRing_of_surjective

Modified Mathlib/RingTheory/Nullstellensatz.lean