Ideal

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

Statistics

Metric	Count
Definitions `IsLocal`, `jacobson`, `jacobson`	3
Theorems `le_jacobson`, `mem_jacobson_or_exists_inv`, `out`, `comap_jacobson`, `comap_jacobson_of_surjective`, `eq_jacobson_iff_notMem`, `eq_jacobson_iff_sInf_maximal`, `eq_jacobson_iff_sInf_maximal'`, `exists_mul_add_sub_mem_of_mem_jacobson`, `exists_mul_sub_mem_of_sub_one_mem_jacobson`, `instIsTwoSidedJacobson`, `isLocal_iff`, `isLocal_of_isMaximal_radical`, `isRadical_jacobson`, `isRadical_of_eq_jacobson`, `isUnit_of_sub_one_mem_jacobson_bot`, `isMaximal`, `jacobson_bot`, `jacobson_eq_bot`, `jacobson_eq_iff_jacobson_quotient_eq_bot`, `jacobson_eq_self_of_isMaximal`, `jacobson_eq_top_iff`, `jacobson_idem`, `jacobson_mono`, `jacobson_radical_eq_jacobson`, `jacobson_top`, `le_jacobson`, `map_jacobson_of_bijective`, `map_jacobson_of_surjective`, `mem_jacobson_bot`, `mem_jacobson_iff`, `radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot`, `radical_le_jacobson`, `ringJacobson_le_jacobson`, `asIdeal_jacobson`, `mem_jacobson_iff`	36
Total	39

Ideal

Definitions

Name	Category	Theorems
`IsLocal` 📖	CompData	2 math math: `isLocal_of_isMaximal_radical`, `isLocal_iff`
`jacobson` 📖	CompOp	44 math math: `eq_jacobson_iff_sInf_maximal`, `jacobson_eq_radical`, `comap_jacobson_of_surjective`, `jacobson.isMaximal`, `isJacobsonRing_iff_prime_eq`, `isRadical_jacobson`, `jacobson_bot`, `IsLocalRing.maximalIdeal_le_jacobson`, `instIsTwoSidedJacobson`, `jacobson_bot_polynomial_le_sInf_map_maximal`, `jacobson_eq_top_iff`, `jacobson_eq_self_of_isMaximal`, `eq_jacobson_iff_sInf_maximal'`, `jacobson_radical_eq_jacobson`, `mem_jacobson_iff`, `TwoSidedIdeal.asIdeal_jacobson`, `radical_eq_jacobson`, `IsJacobsonRing.out`, `IsAdicComplete.le_jacobson_bot`, `Polynomial.jacobson_bot_of_integral_localization`, `IsLocal.le_jacobson`, `eq_jacobson_iff_notMem`, `matrix_jacobson_le`, `radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot`, `jacobson_mono`, `jacobson_eq_iff_jacobson_quotient_eq_bot`, `IsArtinianRing.isNilpotent_jacobson_bot`, `radical_le_jacobson`, `ringJacobson_le_jacobson`, `jacobson_top`, `jacobson_idem`, `IsLocalRing.jacobson_eq_maximalIdeal`, `isJacobsonRing_iff`, `isLocal_iff`, `IsLocal.mem_jacobson_or_exists_inv`, `map_jacobson_of_bijective`, `HenselianRing.jac`, `map_jacobson_of_surjective`, `IsArtinianRing.jacobson_eq_radical`, `le_jacobson`, `IsLocal.out`, `comap_jacobson`, `IsJacobsonRing.out'`, `mem_jacobson_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_jacobson` 📖	mathematical	—	`comap` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `jacobson` `InfSet.sInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Set.image` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `IsMaximal`	—	`RingHom.instRingHomClass` `comap_sInf'` `sInf_eq_iInf`
`comap_jacobson_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`comap` `RingHom.instRingHomClass` `jacobson`	—	`RingHom.instRingHomClass` `le_antisymm` `top_inf_eq` `sInf_insert` `comap_sInf'` `sInf_eq_iInf` `iInf_le_iInf_of_subset` `comap_map_of_surjective` `sup_le_iff` `le_of_eq` `le_trans` `comap_mono` `bot_le` `le_sup_left` `map_eq_top_or_isMaximal_of_surjective` `Set.mem_insert` `Set.mem_insert_of_mem` `le_map_of_comap_le_of_surjective` `comap_sInf` `sInf_le` `comap_isMaximal_of_surjective`
`eq_jacobson_iff_notMem` 📖	mathematical	—	`jacobson` `Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsMaximal` `SetLike.instMembership` `Submodule.setLike`	—	`Mathlib.Tactic.Push.not_forall_eq` `mem_sInf` `jacobson.eq_1` `le_antisymm` `Mathlib.Tactic.Contrapose.contrapose₁` `le_jacobson`
`eq_jacobson_iff_sInf_maximal` 📖	mathematical	—	`jacobson` `IsMaximal` `Ring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `InfSet.sInf` `Submodule.instInfSet`	—	`le_antisymm` `mem_sInf` `le_sInf_iff` `le_of_eq` `Submodule.mem_top` `le_jacobson`
`eq_jacobson_iff_sInf_maximal'` 📖	mathematical	—	`jacobson` `Top.top` `Ideal` `Ring.toSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `InfSet.sInf` `Submodule.instInfSet`	—	`eq_jacobson_iff_sInf_maximal` `IsMaximal.out` `eq_top_iff` `le_of_lt`
`exists_mul_add_sub_mem_of_mem_jacobson` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mem_jacobson_iff` `mul_add` `Distrib.leftDistribClass` `mul_one`
`exists_mul_sub_mem_of_sub_one_mem_jacobson` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_add_cancel` `exists_mul_add_sub_mem_of_mem_jacobson`
`instIsTwoSidedJacobson` 📖	mathematical	—	`IsTwoSided` `Ring.toSemiring` `jacobson`	—	`mem_sInf` `Submodule.smul_mem` `Semigroup.opposite_smulCommClass` `mul_mem_right` `isMaximal_iff` `one_mul` `mem_span_singleton_sup` `mul_mem_left` `le_sup_right` `mem_sup_left` `mem_span_singleton_self` `sub_mul` `mul_assoc` `eq_sub_iff_add_eq` `add_comm` `mul_one` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `sub_add_cancel`
`isLocal_iff` 📖	mathematical	—	`IsLocal` `IsMaximal` `Ring.toSemiring` `CommRing.toRing` `jacobson`	—	`IsLocal.out`
`isLocal_of_isMaximal_radical` 📖	mathematical	—	`IsLocal`	—	`le_antisymm` `le_sInf` `IsPrime.radical_le_iff` `IsMaximal.isPrime` `sInf_le` `le_radical`
`isRadical_jacobson` 📖	mathematical	—	`IsRadical` `CommRing.toCommSemiring` `jacobson` `CommRing.toRing`	—	`isRadical_of_eq_jacobson` `jacobson_idem`
`isRadical_of_eq_jacobson` 📖	mathematical	`jacobson` `CommRing.toRing`	`IsRadical` `CommRing.toCommSemiring`	—	`LE.le.trans` `radical_le_jacobson` `Eq.le`
`isUnit_of_sub_one_mem_jacobson_bot` 📖	mathematical	`Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `Bot.bot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`exists_mul_sub_mem_of_sub_one_mem_jacobson` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_comm` `sub_eq_zero` `mem_bot`
`jacobson_bot` 📖	mathematical	—	`jacobson` `Bot.bot` `Ideal` `Ring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.jacobson`	—	—
`jacobson_eq_bot` 📖	—	`jacobson` `Bot.bot` `Ideal` `Ring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`eq_bot_iff` `le_jacobson`
`jacobson_eq_iff_jacobson_quotient_eq_bot` 📖	mathematical	—	`jacobson` `CommRing.toRing` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Quotient.instRingQuotient` `Bot.bot` `Quotient.semiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.toSemiring`	—	`instIsTwoSided_1` `Submodule.Quotient.mk_surjective` `map_quotient_self` `map_jacobson_of_surjective` `le_of_eq` `RingHom.instRingHomClass` `mk_ker` `RingHom.ker_eq_comap_bot` `comap_jacobson_of_surjective`
`jacobson_eq_self_of_isMaximal` 📖	mathematical	—	`jacobson`	—	`le_antisymm` `sInf_le` `le_of_eq` `le_jacobson`
`jacobson_eq_top_iff` 📖	mathematical	—	`jacobson` `Top.top` `Ideal` `Ring.toSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`by_contradiction` `exists_le_maximal` `lt_top_iff_ne_top` `lt_of_le_of_lt` `sInf_le` `IsMaximal.ne_top` `eq_top_iff` `le_sInf`
`jacobson_idem` 📖	mathematical	—	`jacobson`	—	`le_antisymm` `sInf_le_sInf` `sInf_le` `le_jacobson`
`jacobson_mono` 📖	mathematical	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`jacobson`	—	`jacobson.eq_1` `mem_sInf`
`jacobson_radical_eq_jacobson` 📖	mathematical	—	`jacobson` `CommRing.toRing` `radical` `CommRing.toCommSemiring`	—	`le_antisymm` `le_trans` `le_of_eq` `radical_eq_sInf` `sInf_le_sInf` `sInf_le` `IsMaximal.isPrime` `jacobson_mono` `le_radical`
`jacobson_top` 📖	mathematical	—	`jacobson` `Top.top` `Ideal` `Ring.toSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`eq_top_iff` `le_jacobson`
`le_jacobson` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson`	—	`mem_sInf`
`map_jacobson_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`map` `jacobson`	—	`map_jacobson_of_surjective` `le_trans` `RingHom.instRingHomClass` `le_of_eq` `RingHom.injective_iff_ker_eq_bot` `bot_le`
`map_jacobson_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass`	`map` `jacobson`	—	`RingHom.instRingHomClass` `le_trans` `map_sInf` `le_antisymm` `sInf_le_sInf` `le_comap_of_map_le` `comap_isMaximal_of_surjective` `map_comap_of_surjective` `sInf_le_sInf_of_subset_insert_top` `map_eq_top_or_isMaximal_of_surjective` `Set.mem_insert` `Set.mem_insert_of_mem` `map_mono`
`mem_jacobson_bot` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `Bot.bot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`mem_jacobson_iff` `isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `add_mul` `Distrib.rightDistribClass` `one_mul` `sub_eq_zero` `mul_right_comm` `mul_comm` `Submodule.mem_bot` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero`
`mem_jacobson_iff` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`by_cases` `Submodule.mem_sup` `eq_top_iff_one` `mem_span_singleton'` `mul_assoc` `mul_add_one` `Distrib.leftDistribClass` `neg_sub` `add_sub_cancel_right` `Submodule.neg_mem` `exists_le_maximal` `IsMaximal.out` `sub_mem` `LE.le.trans` `le_sup_right` `subset_span` `mul_mem_left` `add_sub_cancel_left` `mem_sInf` `le_trans` `le_sup_left` `by_contradiction` `IsMaximal.exists_inv` `neg_mul` `sub_eq_iff_eq_add` `sub_add_cancel` `sub_sub_cancel`
`radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot` 📖	mathematical	—	`radical` `CommRing.toCommSemiring` `jacobson` `CommRing.toRing` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `instHasQuotient_1` `Quotient.commSemiring` `Bot.bot` `Quotient.semiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Quotient.instRingQuotient` `Ring.toSemiring`	—	`instIsTwoSided_1` `Submodule.Quotient.mk_surjective` `map_quotient_self` `map_jacobson_of_surjective` `le_of_eq` `RingHom.instRingHomClass` `mk_ker` `map_radical_of_surjective` `RingHom.ker_eq_comap_bot` `comap_jacobson_of_surjective` `comap_radical`
`radical_le_jacobson` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `radical` `jacobson` `CommRing.toRing`	—	`le_sInf` `sInf_le` `IsMaximal.isPrime` `radical_eq_sInf`
`ringJacobson_le_jacobson` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.jacobson` `jacobson`	—	`Eq.trans_le` `jacobson_bot` `jacobson_mono` `bot_le`

Ideal.IsLocal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_jacobson` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal.jacobson` `CommRing.toRing`	—	`Ideal.exists_le_maximal` `le_trans` `le_of_eq` `Ideal.IsMaximal.eq_of_le` `out` `Ideal.IsMaximal.out` `sInf_le`
`mem_jacobson_or_exists_inv` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`by_cases` `Submodule.mem_sup` `Ideal.eq_top_iff_one` `Ideal.mem_span_singleton` `mul_comm` `neg_sub` `add_sub_cancel_right` `Submodule.neg_mem` `le_trans` `le_sup_right` `le_jacobson` `le_sup_left` `dvd_refl`
`out` 📖	mathematical	—	`Ideal.IsMaximal` `Ring.toSemiring` `CommRing.toRing` `Ideal.jacobson`	—	—

Ideal.jacobson

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `Ring.toSemiring` `Ideal.jacobson`	—	`Ideal.IsMaximal.out` `Ideal.jacobson_eq_top_iff` `lt_of_le_of_lt` `Ideal.le_jacobson`

TwoSidedIdeal

Definitions

Name	Category	Theorems
`jacobson` 📖	CompOp	4 math math: `matrix_jacobson_bot`, `jacobson_matrix`, `mem_jacobson_iff`, `asIdeal_jacobson`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asIdeal_jacobson` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `asIdeal` `jacobson` `Ideal.jacobson`	—	`Ideal.ext` `Ideal.asIdeal_toTwoSided`
`mem_jacobson_iff` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `jacobson` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—

---

← Back to Index