Documentation Verification Report

Radical

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

Statistics

Metric	Count
Definitions `jacobson`, `jacobson`	2
Theorems `comap_jacobson_of_bijective`, `comap_jacobson_of_ker_le`, `jacobson_eq_bot_of_injective`, `jacobson_le_of_eq_bot`, `jacobson_lt_top`, `jacobson_pi_eq_bot`, `jacobson_pi_le`, `jacobson_quotient_jacobson`, `jacobson_quotient_of_le`, `le_comap_jacobson`, `map_jacobson_le`, `map_jacobson_of_bijective`, `map_jacobson_of_ker_le`, `coe_jacobson_quotient`, `instIsTwoSidedJacobson`, `jacobson_eq_sInf_isMaximal`, `jacobson_le_of_eq_bot`, `jacobson_le_of_isMaximal`, `jacobson_lt_top`, `jacobson_quotient_jacobson`, `jacobson_quotient_of_le`, `jacobson_smul_top_le`, `le_comap_jacobson`, `map_jacobson_le`, `map_jacobson_of_ker_le`, `eq_bot_of_le_jacobson_smul`, `jacobson_smul_lt`, `jacobson_smul_lt_top`	28
Total	30

Module

Definitions

Name	Category	Theorems
`jacobson` 📖	CompOp	13 math math: `Ring.coe_jacobson_quotient`, `jacobson_lt_top`, `Ring.jacobson_smul_top_le`, `map_jacobson_of_bijective`, `jacobson_pi_le`, `IsSimpleModule.jacobson_eq_bot`, `comap_jacobson_of_bijective`, `IsSemisimpleModule.jacobson_le_ker`, `IsArtinian.isSemisimpleModule_iff_jacobson`, `map_jacobson_le`, `IsSemisimpleModule.jacobson_eq_bot`, `jacobson_quotient_jacobson`, `le_comap_jacobson`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_jacobson_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Submodule.comap` `jacobson`	—	`comap_jacobson_of_ker_le` `LinearMap.ker_eq_bot`
`comap_jacobson_of_ker_le` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.ker` `jacobson`	`Submodule.comap`	—	`map_jacobson_of_ker_le` `Submodule.comap_map_eq_self`
`jacobson_eq_bot_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `jacobson` `Bot.bot` `Submodule` `Submodule.instBot`	—	—	`le_bot_iff` `LE.le.trans` `le_comap_jacobson` `Eq.le` `LinearMap.ker_eq_bot`
`jacobson_le_of_eq_bot` 📖	mathematical	`jacobson` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Bot.bot` `Submodule.instBot`	`Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`Submodule.ker_mkQ` `RingHomSurjective.ids`
`jacobson_lt_top` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `jacobson` `Top.top` `Submodule.instTop`	—	`IsCoatomic.eq_top_or_exists_le_coatom` `bot_ne_top` `Submodule.instNontrivial` `LE.le.trans_lt` `sInf_le` `Set.mem_setOf` `Ne.lt_top`
`jacobson_pi_eq_bot` 📖	mathematical	`jacobson` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	`Pi.addCommGroup` `Pi.module`	—	`le_bot_iff` `LE.le.trans` `jacobson_pi_le` `Submodule.pi_univ_bot`
`jacobson_pi_le` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Pi.module` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `jacobson` `Submodule.pi` `Set.univ`	—	`sInf_eq_iInf'` `Submodule.comap_iInf` `RingHomSurjective.ids` `iInf_le_of_le` `Submodule.isCoatom_comap_iff` `LinearMap.proj_surjective` `le_rfl`
`jacobson_quotient_jacobson` 📖	mathematical	—	`jacobson` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Bot.bot` `Submodule.instBot`	—	`RingHomSurjective.ids` `jacobson_quotient_of_le` `le_rfl` `Submodule.mkQ_map_self`
`jacobson_quotient_of_le` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `jacobson`	`HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.mkQ`	—	`RingHomSurjective.ids` `map_jacobson_of_ker_le` `Submodule.mkQ_surjective` `Submodule.ker_mkQ`
`le_comap_jacobson` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `jacobson` `Submodule.comap`	—	`jacobson.eq_1` `sInf_eq_iInf'` `Submodule.comap_iInf` `le_iInf_iff` `Submodule.isCoatom_comap_or_eq_top` `Submodule.mem_sInf` `Submodule.mem_top`
`map_jacobson_le` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map` `jacobson`	—	`Submodule.map_le_iff_le_comap` `le_comap_jacobson`
`map_jacobson_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Submodule.map` `jacobson`	—	`map_jacobson_of_ker_le` `LinearMap.ker_eq_bot`
`map_jacobson_of_ker_le` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.ker` `jacobson`	`Submodule.map`	—	`le_antisymm` `map_jacobson_le` `jacobson.eq_1` `sInf_eq_iInf'` `Submodule.map_iInf_of_ker_le` `le_iInf` `sInf_le` `Submodule.isCoatom_map_of_ker_le` `le_iInf_iff`

Ring

Definitions

Name	Category	Theorems
`jacobson` 📖	CompOp	23 math math: `jacobson_eq_nilradical_of_krullDimLE_zero`, `coe_jacobson_quotient`, `IsSemisimpleModule.jacobson_le_annihilator`, `Ideal.jacobson_bot`, `jacobson_smul_top_le`, `nilradical_le_jacobson`, `Submodule.jacobson_smul_lt_top`, `IsSemiprimaryRing.isNilpotent`, `jacobson_le_of_isMaximal`, `IsSemiprimaryRing.isSemisimpleRing`, `map_jacobson_le`, `instIsTwoSidedJacobson`, `Ideal.ringJacobson_le_jacobson`, `Submodule.FG.jacobson_smul_lt`, `IsSemisimpleRing.jacobson_eq_bot`, `isSemiprimaryRing_iff`, `le_comap_jacobson`, `IsArtinianRing.isSemisimpleRing_iff_jacobson`, `IsSemiprimaryRing.isNoetherianRing_iff_jacobson_fg`, `jacobson_lt_top`, `IsLocalRing.ringJacobson_eq_maximalIdeal`, `jacobson_quotient_jacobson`, `jacobson_eq_sInf_isMaximal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_jacobson_quotient` 📖	mathematical	—	`SetLike.coe` `Ideal` `HasQuotient.Quotient` `toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.addCommGroup` `toAddCommGroup` `Submodule.Quotient.module` `Module.jacobson`	—	`jacobson.eq_1` `Ideal.Quotient.instRingHomSurjectiveQuotientMk` `Module.map_jacobson_of_ker_le` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Set.image_id`
`instIsTwoSidedJacobson` 📖	mathematical	—	`Ideal.IsTwoSided` `toSemiring` `jacobson`	—	`Module.le_comap_jacobson` `RingHomSurjective.ids`
`jacobson_eq_sInf_isMaximal` 📖	mathematical	—	`jacobson` `InfSet.sInf` `Ideal` `toSemiring` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `Ideal.IsMaximal`	—	—
`jacobson_le_of_eq_bot` 📖	mathematical	`jacobson` `HasQuotient.Quotient` `Ideal` `toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`Module.jacobson_le_of_eq_bot` `le_bot_iff` `SetLike.coe_subset_coe` `instIsConcreteLE` `coe_jacobson_quotient`
`jacobson_le_of_isMaximal` 📖	mathematical	—	`Ideal` `toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson`	—	`jacobson_eq_sInf_isMaximal` `sInf_le`
`jacobson_lt_top` 📖	mathematical	—	`Ideal` `toSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `Top.top` `Submodule.instTop`	—	`Module.jacobson_lt_top` `Ideal.instIsCoatomic`
`jacobson_quotient_jacobson` 📖	mathematical	—	`jacobson` `HasQuotient.Quotient` `Ideal` `toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `instIsTwoSidedJacobson` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`instIsTwoSidedJacobson` `Ideal.Quotient.instRingHomSurjectiveQuotientMk` `jacobson_quotient_of_le` `le_rfl` `SetLike.ext'` `RingHomSurjective.ids` `SetLike.ext'_iff` `Submodule.mkQ_map_self`
`jacobson_quotient_of_le` 📖	mathematical	`Ideal` `toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson`	`HasQuotient.Quotient` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Submodule.map` `Ideal.Quotient.instRingHomSurjectiveQuotientMk` `RingHom.toSemilinearMap`	—	`Ideal.Quotient.instRingHomSurjectiveQuotientMk` `Module.map_jacobson_of_ker_le` `Ideal.Quotient.mk_surjective` `Submodule.ker_mkQ`
`jacobson_smul_top_le` 📖	mathematical	—	`Submodule` `toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `jacobson` `Top.top` `Submodule.instTop` `Module.jacobson`	—	`IsScalarTower.left` `Submodule.smul_le` `Module.le_comap_jacobson` `RingHomSurjective.ids`
`le_comap_jacobson` 📖	mathematical	—	`Ideal` `toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `jacobson` `Ideal.comap` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`Module.le_comap_jacobson`
`map_jacobson_le` 📖	mathematical	—	`Submodule` `toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map` `RingHom.toSemilinearMap` `jacobson`	—	`Module.map_jacobson_le`
`map_jacobson_of_ker_le` 📖	mathematical	`Ideal` `toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `jacobson`	`Submodule.map` `RingHom.toSemilinearMap`	—	`RingHom.instRingHomClass` `Module.map_jacobson_of_ker_le` `RingHom.surjective`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_smul_lt_top` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.jacobson` `Top.top` `instTop`	—	`LE.le.trans_lt` `IsScalarTower.left` `LE.le.trans` `smul_mono_right` `instCovariantClassHSMulLe_1` `le_top` `Ring.jacobson_smul_top_le` `Module.jacobson_lt_top`

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_of_le_jacobson_smul` 📖	mathematical	`Submodule.FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.jacobson`	`Bot.bot` `Submodule.instBot`	—	`IsScalarTower.left` `Mathlib.Tactic.Contrapose.contrapose₁` `LT.lt.not_ge` `jacobson_smul_lt`
`jacobson_smul_lt` 📖	mathematical	`Submodule.FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.jacobson`	—	`IsScalarTower.left` `RingHomSurjective.ids` `Submodule.map_smul''` `Submodule.map_top` `Submodule.range_subtype` `Submodule.map_strictMono_of_injective` `Submodule.injective_subtype` `Submodule.jacobson_smul_lt_top` `Submodule.nontrivial_iff_ne_bot` `Module.Finite.instIsCoatomicSubmodule` `Module.Finite.iff_fg`

---

← Back to Index