Documentation Verification Report

Ring

📁 Source: Mathlib/RingTheory/Jacobson/Ring.lean

Statistics

Metric	Count
Definitions `IsJacobsonRing`, `orderIsoOfMaximal`	2
Theorems `radical_eq_jacobson`, `out`, `out'`, `isMaximal_iff_isMaximal_disjoint`, `isMaximal_of_isMaximal_disjoint`, `comp_C_integral_of_surjective_of_isJacobsonRing`, `isJacobsonRing`, `isJacobsonRing_MvPolynomial_fin`, `quotient_mk_comp_C_isIntegral_of_isJacobsonRing`, `comp_C_integral_of_surjective_of_isJacobsonRing`, `instIsJacobsonRing`, `isIntegral_isLocalization_polynomial_quotient`, `isJacobsonRing_polynomial_iff_isJacobsonRing`, `isJacobsonRing_polynomial_of_isJacobsonRing`, `isMaximal_comap_C_of_isJacobsonRing`, `isMaximal_comap_C_of_isMaximal`, `jacobson_bot_of_integral_localization`, `mem_closure_X_union_C`, `quotient_mk_comp_C_isIntegral_of_isJacobsonRing`, `isJacobsonRing`, `finite_iff_finiteType_of_isJacobsonRing`, `finite_of_algHom_finiteType_of_isJacobsonRing`, `finite_of_algHom_finiteType_of_isJacobsonRing`, `finite_of_finite_type_of_isJacobsonRing`, `instIsJacobsonRingOfIsArtinianRing`, `isJacobsonRing_iff`, `isJacobsonRing_iff_prime_eq`, `isJacobsonRing_iff_sInf_maximal`, `isJacobsonRing_iff_sInf_maximal'`, `isJacobsonRing_iso`, `isJacobsonRing_localization`, `isJacobsonRing_of_finiteType`, `isJacobsonRing_of_isIntegral`, `isJacobsonRing_of_isIntegral'`, `isJacobsonRing_of_surjective`, `isJacobsonRing_quotient`	36
Total	38

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`radical_eq_jacobson` 📖	mathematical	—	`radical` `CommRing.toCommSemiring` `jacobson` `CommRing.toRing`	—	`le_antisymm` `le_sInf` `IsPrime.radical_le_iff` `IsMaximal.isPrime` `jacobson_mono` `le_radical` `IsJacobsonRing.out` `radical_isRadical`

IsJacobsonRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	`Ideal.IsRadical` `CommRing.toCommSemiring`	`Ideal.jacobson` `CommRing.toRing`	—	`isJacobsonRing_iff`
`out'` 📖	mathematical	`Ideal.IsRadical` `CommRing.toCommSemiring`	`Ideal.jacobson` `CommRing.toRing`	—	—

IsLocalization

Definitions

Name	Category	Theorems
`orderIsoOfMaximal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal_iff_isMaximal_disjoint` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `Ideal.IsMaximal.isPrime` `Set.disjoint_left` `isPrime_iff_isPrime_disjoint` `Submonoid.mem_powers` `Mathlib.Tactic.Push.not_forall_eq` `Ideal.mem_sInf` `Submodule.mem_toAddSubmonoid` `Ideal.jacobson.eq_1` `IsJacobsonRing.out` `Ideal.IsPrime.isRadical` `comap_map_of_isPrime_disjoint` `Ideal.disjoint_powers_iff_notMem` `isPrime_of_isPrime_disjoint` `Ideal.map_mono` `map_comap` `Ideal.IsMaximal.out` `lt_of_le_of_ne` `Ideal.IsPrime.ne_top'` `Ideal.IsMaximal.ne_top` `Ideal.eq_top_of_isUnit_mem` `map_units` `Ideal.IsMaximal.of_isLocalization_of_disjoint`
`isMaximal_of_isMaximal_disjoint` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHom.instRingHomClass` `isMaximal_iff_isMaximal_disjoint` `comap_map_of_isPrime_disjoint` `Ideal.IsMaximal.isPrime` `Ideal.disjoint_powers_iff_notMem` `Ideal.IsPrime.isRadical`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_C_integral_of_surjective_of_isJacobsonRing` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	`RingHom.IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `RingHom.comp` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `C`	—	`nonempty_fintype` `AlgEquiv.surjective` `RingHom.instRingHomClass` `RingHom.ker_isMaximal_of_surjective` `Ideal.instIsTwoSided_1` `ringHom_ext` `RingHom.comp_assoc` `RingHom.IsIntegral.trans` `quotient_mk_comp_C_isIntegral_of_isJacobsonRing` `RingHom.isIntegral_of_surjective` `Function.Surjective.of_comp` `RingHom.ext` `AlgEquiv.commutes'`
`isJacobsonRing` 📖	mathematical	—	`IsJacobsonRing` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.commRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`nonempty_fintype` `isJacobsonRing_iso` `isJacobsonRing_MvPolynomial_fin`
`isJacobsonRing_MvPolynomial_fin` 📖	mathematical	—	`IsJacobsonRing` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.commRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`isJacobsonRing_iso` `Fin.isEmpty'` `PEmpty.instIsEmpty` `Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing`
`quotient_mk_comp_C_isIntegral_of_isJacobsonRing` 📖	mathematical	—	`RingHom.IsIntegral` `HasQuotient.Quotient` `MvPolynomial` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ideal.instIsTwoSided_1` `C`	—	`Ideal.instIsTwoSided_1`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_C_integral_of_surjective_of_isJacobsonRing` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	`RingHom.IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `RingHom.comp` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `C`	—	`RingHom.instRingHomClass` `RingHom.ker_isMaximal_of_surjective` `Ideal.instIsTwoSided_1` `ringHom_ext'` `RingHom.comp_assoc` `RingHom.IsIntegral.trans` `quotient_mk_comp_C_isIntegral_of_isJacobsonRing` `RingHom.isIntegral_of_surjective` `Function.Surjective.of_comp`
`instIsJacobsonRing` 📖	mathematical	—	`IsJacobsonRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	—	`isJacobsonRing_polynomial_iff_isJacobsonRing`
`isIntegral_isLocalization_polynomial_quotient` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`RingHom.IsIntegral` `CommRing.toRing` `IsLocalization.map` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.comap` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `ring` `RingHom.instFunLike` `C` `RingHom.instRingHomClass` `Ideal.Quotient.commSemiring` `Submonoid.powers` `semiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `leadingCoeff` `map` `Ideal.instIsTwoSided_1` `commRing` `Submonoid.map` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.quotientMap` `le_rfl` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Submonoid.le_comap_map`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `le_rfl` `Submonoid.le_comap_map` `IsLocalization.surj` `IsIntegral.of_mem_closure''` `RingHom.isIntegralElem_localization_at_leadingCoeff` `eval₂_map` `hom_eval₂` `Ideal.Quotient.eq_zero_iff_mem` `eval₂_C_X` `pow_one` `degree_le_zero_iff` `monic_X_sub_C` `eval₂_sub` `eval₂_X` `eval₂_C` `sub_eq_zero` `RingHom.comp_apply` `IsLocalization.map_comp` `Ideal.Quotient.mk_surjective` `Subring.mem_closure_image_of` `mem_closure_X_union_C` `isUnit_iff_exists_inv'` `instIsDedekindFiniteMonoid` `IsLocalization.map_units` `RingHom.IsIntegralElem.of_mul_unit` `RingHom.map_one` `RingHom.map_mul`
`isJacobsonRing_polynomial_iff_isJacobsonRing` 📖	mathematical	—	`IsJacobsonRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	—	`isJacobsonRing_of_surjective` `eval₂_C` `isJacobsonRing_polynomial_of_isJacobsonRing`
`isJacobsonRing_polynomial_of_isJacobsonRing` 📖	mathematical	—	`IsJacobsonRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	—	`isJacobsonRing_iff_prime_eq` `Ideal.instIsTwoSided_1` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `RingHom.rangeRestrict_surjective` `RingHom.instRingHomClass` `Ideal.polynomial_mem_ideal_of_coeff_mem_ideal` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Ideal.mem_comap` `Ideal.Quotient.eq_zero_iff_mem` `RingHom.comp_apply` `coeff_map` `isJacobsonRing_of_surjective` `map_surjective` `Ideal.map_isPrime_of_surjective` `Subring.instIsDomainSubtypeMem` `Ideal.Quotient.isDomain` `Ideal.eq_zero_of_polynomial_mem_map_range` `le_antisymm` `le_trans` `le_sup_of_le_left` `le_rfl` `le_of_eq` `Ideal.comap_map_of_surjective` `Ideal.map_jacobson_of_surjective` `sup_le` `Ideal.le_jacobson`
`isMaximal_comap_C_of_isJacobsonRing` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.comap` `Polynomial` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1` `Ideal.mk_ker` `RingHom.ker_eq_comap_bot` `Ideal.comap_comap` `Ideal.bot_quotient_isMaximal_iff` `Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'` `quotient_mk_comp_C_isIntegral_of_isJacobsonRing`
`isMaximal_comap_C_of_isMaximal` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.comap` `Polynomial` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `Ideal.comap_isPrime` `Ideal.IsMaximal.isPrime'` `Submodule.nonzero_mem_of_bot_lt` `Ideal.bot_lt_of_maximal` `nontrivial` `Ideal.polynomial_not_isField` `Ideal.instIsTwoSided_1` `le_rfl` `Ideal.bot_quotient_isMaximal_iff` `map_injective` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `eq_bot_iff` `Ideal.Quotient.eq_zero_iff_mem` `map_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `Ideal.Quotient.noZeroDivisors` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.quotientMap_injective` `trans` `Ideal.instIsTwoSidedComap` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `RingHom.map_zero` `Ideal.map_bot` `Ideal.IsMaximal.map_bijective` `IsField.localization_map_bijective` `Ideal.Quotient.maximal_ideal_iff_isField_quotient` `Localization.isLocalization` `Submonoid.le_comap_map` `le_antisymm` `bot_le` `Ideal.comap_bot_le_of_injective` `IsLocalization.map_injective_of_injective` `Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'` `isIntegral_isLocalization_polynomial_quotient` `IsLocalization.comap_map_of_isPrime_disjoint` `Ideal.isPrime_bot` `IsDomain.toNontrivial` `Ideal.Quotient.isDomain` `disjoint_iff_inf_le` `IsLocalization.isMaximal_iff_isMaximal_disjoint` `isJacobsonRing_quotient`
`jacobson_bot_of_integral_localization` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.IsIntegral` `CommRing.toRing` `IsLocalization.map` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submonoid.map` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.le_comap_map`	`Ideal.jacobson` `CommRing.toRing` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.le_comap_map` `map_le_nonZeroDivisors_of_injective` `IsDomain.to_noZeroDivisors` `powers_le_nonZeroDivisors_of_noZeroDivisors` `Ideal.comap_isPrime` `Ideal.IsMaximal.isPrime'` `Ideal.isPrime_bot` `IsDomain.toNontrivial` `Ideal.instIsTwoSided_1` `Ideal.Quotient.isDomain` `Ideal.Quotient.noZeroDivisors` `IsLocalization.map_comp` `le_rfl` `Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'` `IsLocalization.isMaximal_iff_isMaximal_disjoint` `Ideal.comap_comap` `Ideal.bot_quotient_isMaximal_iff` `Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'` `RingHom.IsIntegral.tower_bot` `Ideal.quotientMap_injective` `Ideal.instIsTwoSidedComap` `le_of_eq` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `RingHom.IsIntegral.trans` `RingHom.isIntegral_of_surjective` `IsLocalization.surjective_quotientMap_of_maximal_of_localization` `RingHom.IsIntegral.quotient` `Ideal.comp_quotientMap_eq_of_comp_eq` `eq_bot_iff` `Ideal.comap_bot_le_of_injective` `RingHom.ker_eq_comap_bot` `RingHom.injective_iff_ker_eq_bot` `IsLocalization.injective` `isJacobsonRing_localization` `isJacobsonRing_of_isIntegral'` `le_trans` `IsJacobsonRing.out` `Ideal.isRadical_bot_of_noZeroDivisors` `IsLocalization.isDomain_of_le_nonZeroDivisors` `Ideal.comap_jacobson` `sInf_le_sInf` `bot_le`
`mem_closure_X_union_C` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `Subring` `Ring.toNonAssocRing` `ring` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `Set` `Set.instInsert` `X` `setOf` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`induction_on` `Subring.subset_closure` `Set.mem_insert_of_mem` `degree_C_le` `Subring.add_mem` `pow_succ` `mul_assoc` `Subring.mul_mem` `Set.mem_insert`
`quotient_mk_comp_C_isIntegral_of_isJacobsonRing` 📖	mathematical	—	`RingHom.IsIntegral` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `ring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `commRing` `RingHom.comp` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `C`	—	`RingHom.instRingHomClass` `Ideal.comap_isPrime` `Ideal.IsMaximal.isPrime'` `Ideal.instIsTwoSided_1` `map_surjective` `Quotient.mk_surjective` `Ideal.comap_map_of_surjective` `le_antisymm` `le_sup_of_le_left` `le_rfl` `sup_le` `Ideal.polynomial_mem_ideal_of_coeff_mem_ideal` `Ideal.Quotient.eq_zero_iff_mem` `coeff_map` `ext_iff` `RingHom.IsIntegral.tower_bot` `Ideal.le_comap_map` `Ideal.injective_quotient_le_comap_map` `Ideal.quotient_mk_maps_eq` `RingHom.IsIntegral.trans` `RingHom.isIntegral_of_surjective` `Ideal.map_eq_top_or_isMaximal_of_surjective` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `Ideal.comap_top` `Ideal.IsMaximal.ne_top` `IsDomain.toNontrivial` `Ideal.Quotient.isDomain` `isJacobsonRing_quotient` `Ideal.Quotient.mk_surjective` `Ideal.mem_comap` `coe_mapRingHom` `map_C`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_finiteType_of_isJacobsonRing` 📖	mathematical	—	`Finite` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `FiniteType`	—	`FiniteType.of_finite` `finite_of_finite_type_of_isJacobsonRing`
`finite_of_algHom_finiteType_of_isJacobsonRing` 📖	mathematical	—	`Finite` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`finite_of_algHom_finiteType_of_isJacobsonRing`

RingHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isJacobsonRing` 📖	mathematical	—	`IsJacobsonRing`	—	`isJacobsonRing_of_finiteType`

(root)

Definitions

Name	Category	Theorems
`IsJacobsonRing` 📖	CompData	20 math math: `MvPolynomial.isJacobsonRing`, `Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing`, `isJacobsonRing_of_isIntegral`, `isJacobsonRing_iff_prime_eq`, `isJacobsonRing_iso`, `isJacobsonRing_iff_sInf_maximal`, `instIsJacobsonRingOfIsArtinianRing`, `isJacobsonRing_of_surjective`, `RingHom.FiniteType.isJacobsonRing`, `Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing`, `instIsJacobsonRingOfKrullDimLEOfNatNat`, `Polynomial.instIsJacobsonRing`, `isJacobsonRing_quotient`, `isJacobsonRing_iff_sInf_maximal'`, `isJacobsonRing_of_isIntegral'`, `MvPolynomial.isJacobsonRing_MvPolynomial_fin`, `isJacobsonRing_of_finiteType`, `isJacobsonRing_iff`, `PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace`, `isJacobsonRing_localization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_algHom_finiteType_of_isJacobsonRing` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`Ideal.exists_maximal` `finite_of_finite_type_of_isJacobsonRing` `Algebra.FiniteType.quotient` `Module.Finite.of_injective` `Ideal.instIsTwoSided_1` `isNoetherian_of_isNoetherianRing_of_finite` `RingHomInvPair.ids` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial`
`finite_of_finite_type_of_isJacobsonRing` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Algebra.FiniteType.iff_quotient_mvPolynomial'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing` `Finite.of_fintype` `Algebra.isIntegral_def` `Algebra.IsIntegral.finite`
`instIsJacobsonRingOfIsArtinianRing` 📖	mathematical	—	`IsJacobsonRing`	—	`isJacobsonRing_iff_prime_eq` `Ideal.jacobson_eq_self_of_isMaximal` `IsArtinianRing.isMaximal_of_isPrime`
`isJacobsonRing_iff` 📖	mathematical	—	`IsJacobsonRing` `Ideal.jacobson` `CommRing.toRing`	—	`IsJacobsonRing.out'`
`isJacobsonRing_iff_prime_eq` 📖	mathematical	—	`IsJacobsonRing` `Ideal.jacobson` `CommRing.toRing`	—	`isJacobsonRing_iff` `Ideal.IsPrime.isRadical` `le_antisymm` `Ideal.IsRadical.radical` `Ideal.radical_eq_sInf` `Ideal.mem_sInf` `Set.mem_setOf_eq` `Ideal.jacobson.eq_1` `le_trans`
`isJacobsonRing_iff_sInf_maximal` 📖	mathematical	—	`IsJacobsonRing` `Set` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.IsMaximal` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `InfSet.sInf` `Submodule.instInfSet`	—	`Ideal.eq_jacobson_iff_sInf_maximal` `IsJacobsonRing.out` `Ideal.IsPrime.isRadical` `isJacobsonRing_iff_prime_eq`
`isJacobsonRing_iff_sInf_maximal'` 📖	mathematical	—	`IsJacobsonRing` `Set` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `InfSet.sInf` `Submodule.instInfSet`	—	`Ideal.eq_jacobson_iff_sInf_maximal'` `IsJacobsonRing.out` `Ideal.IsPrime.isRadical` `isJacobsonRing_iff_prime_eq`
`isJacobsonRing_iso` 📖	mathematical	—	`IsJacobsonRing`	—	`isJacobsonRing_of_surjective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.surjective`
`isJacobsonRing_localization` 📖	mathematical	—	`IsJacobsonRing`	—	`isJacobsonRing_iff_prime_eq` `le_antisymm` `RingHom.instRingHomClass` `IsLocalization.isPrime_iff_isPrime_disjoint` `IsJacobsonRing.out` `Ideal.IsPrime.isRadical` `LE.le.trans` `Eq.ge` `IsLocalization.map_comap` `Ideal.map_mono` `Ideal.jacobson.eq_1` `Ideal.mem_sInf` `Ideal.mul_mem_left` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Ideal.IsPrime.mem_or_mem` `Disjoint.le_bot` `Submonoid.mem_powers` `le_trans` `Ideal.comap_sInf'` `sInf_eq_iInf` `iInf_le_iInf_of_subset` `le_of_eq` `IsLocalization.isMaximal_of_isMaximal_disjoint` `IsLocalization.comap_map_of_isPrime_disjoint` `Ideal.IsMaximal.isPrime` `Ideal.disjoint_powers_iff_notMem` `Eq.le` `Ideal.le_jacobson`
`isJacobsonRing_of_finiteType` 📖	mathematical	—	`IsJacobsonRing`	—	`Algebra.FiniteType.iff_quotient_mvPolynomial'` `isJacobsonRing_of_surjective` `MvPolynomial.isJacobsonRing` `Finite.of_fintype`
`isJacobsonRing_of_isIntegral` 📖	mathematical	—	`IsJacobsonRing`	—	`isJacobsonRing_iff_prime_eq` `RingHom.instRingHomClass` `Ideal.comap_eq_top_iff` `Ideal.jacobson_top` `Ideal.Quotient.nontrivial_iff` `Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot` `Ideal.eq_bot_of_comap_eq_bot` `Ideal.Quotient.isDomain` `Ideal.instIsTwoSided_1` `Algebra.IsIntegral.quotient` `eq_bot_iff` `Ideal.comap_isPrime` `Ideal.comap_jacobson` `sInf_le_sInf` `Ideal.exists_ideal_over_maximal_of_isIntegral` `Ideal.comap_bot_le_of_injective` `Ideal.algebraMap_quotient_injective`
`isJacobsonRing_of_isIntegral'` 📖	mathematical	`RingHom.IsIntegral` `CommRing.toRing`	`IsJacobsonRing`	—	`isJacobsonRing_of_isIntegral`
`isJacobsonRing_of_surjective` 📖	mathematical	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom.instFunLike`	`IsJacobsonRing`	—	`isJacobsonRing_iff_sInf_maximal` `RingHom.instRingHomClass` `Ideal.map_eq_top_or_isMaximal_of_surjective` `Ideal.map_comap_of_surjective` `IsJacobsonRing.out'` `Ideal.IsRadical.comap` `Ideal.IsPrime.isRadical` `Ideal.map_sInf` `le_trans` `Ideal.ker_le_comap`
`isJacobsonRing_quotient` 📖	mathematical	—	`IsJacobsonRing` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing`	—	`isJacobsonRing_of_surjective` `Ideal.instIsTwoSided_1`

---

← Back to Index