Commit 2023-07-04 05:50 9b91d86c

View on Github →

feat: port RingTheory.Jacobson (#4338)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'

deleted theorem Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'

Modified Mathlib/RingTheory/IntegralClosure.lean

added theorem RingHom.isIntegral_of_isIntegral_mul_unit

deleted theorem RingHom.is_integral_of_is_integral_mul_unit

added theorem isIntegral_of_mem_closure''

deleted theorem is_integral_of_mem_closure''

Created Mathlib/RingTheory/Jacobson.lean

added theorem Ideal.IsJacobson.out

added theorem Ideal.MvPolynomial.comp_C_integral_of_surjective_of_jacobson

added theorem Ideal.MvPolynomial.isJacobson_MvPolynomial_fin

added theorem Ideal.MvPolynomial.quotient_mk_comp_C_isIntegral_of_jacobson

added theorem Ideal.Polynomial.Subring.mem_closure_image_of

added theorem Ideal.Polynomial.comp_C_integral_of_surjective_of_jacobson

added theorem Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient

added theorem Ideal.Polynomial.isJacobson_polynomial_iff_isJacobson

added theorem Ideal.Polynomial.isJacobson_polynomial_of_isJacobson

added theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson'

added theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson

added theorem Ideal.Polynomial.isMaximal_comap_C_of_isMaximal

added theorem Ideal.Polynomial.jacobson_bot_of_integral_localization

added theorem Ideal.Polynomial.mem_closure_X_union_C

added theorem Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson

added theorem Ideal.disjoint_powers_iff_not_mem

added theorem Ideal.isJacobson_iff

added theorem Ideal.isJacobson_iff_prime_eq

added theorem Ideal.isJacobson_iff_sInf_maximal'

added theorem Ideal.isJacobson_iff_sInf_maximal

added theorem Ideal.isJacobson_iso

added theorem Ideal.isJacobson_localization

added theorem Ideal.isJacobson_of_isIntegral'

added theorem Ideal.isJacobson_of_isIntegral

added theorem Ideal.isJacobson_of_surjective

added theorem Ideal.isMaximal_iff_isMaximal_disjoint

added theorem Ideal.isMaximal_of_isMaximal_disjoint

added def Ideal.orderIsoOfMaximal

added theorem Ideal.radical_eq_jacobson