Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/SimpleRing/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `isSimpleRing`, `iff_injective_ringHom`, `iff_injective_ringHom_or_subsingleton_codomain`, `injective_ringHom_or_subsingleton_codomain`, `instMulOpposite`, `instNontrivial`, `of_eq_bot_or_eq_top`, `one_mem_of_ne_bot`, `one_mem_of_ne_zero_mem`, `injective`	10
Total	10

DivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleRing` 📖	mathematical	—	`IsSimpleRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing`	—	`IsSimpleRing.of_eq_bot_or_eq_top` `toNontrivial` `TwoSidedIdeal.one_mem_iff` `SetLike.exists_of_lt` `instIsConcreteLE` `bot_lt_iff_ne_bot` `inv_mul_cancel₀` `TwoSidedIdeal.mul_mem_left`

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_injective_ringHom` 📖	mathematical	—	`IsSimpleRing` `NonAssocRing.toNonUnitalNonAssocRing` `DFunLike.coe` `RingHom` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike`	—	`iff_injective_ringHom_or_subsingleton_codomain` `subsingleton_or_nontrivial`
`iff_injective_ringHom_or_subsingleton_codomain` 📖	mathematical	—	`IsSimpleRing` `NonAssocRing.toNonUnitalNonAssocRing` `DFunLike.coe` `RingHom` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike`	—	`injective_ringHom_or_subsingleton_codomain` `of_eq_bot_or_eq_top` `le_antisymm` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `TwoSidedIdeal.ker_ringCon_mk'` `TwoSidedIdeal.ker_eq_bot` `bot_le` `le_top` `TwoSidedIdeal.mem_iff` `Quotient.eq'`
`injective_ringHom_or_subsingleton_codomain` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `TwoSidedIdeal.ker_eq_bot` `subsingleton_iff_zero_eq_one` `TwoSidedIdeal.mem_top` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `TwoSidedIdeal.mem_ker` `IsSimpleOrder.eq_bot_or_eq_top` `simple`
`instMulOpposite` 📖	mathematical	—	`IsSimpleRing` `MulOpposite` `MulOpposite.instNonUnitalNonAssocRing`	—	`OrderIso.isSimpleOrder` `simple`
`instNontrivial` 📖	mathematical	—	`Nontrivial`	—	`SetLike.exists_of_lt` `instIsConcreteLE` `bot_lt_top` `IsSimpleOrder.toNontrivial` `simple`
`of_eq_bot_or_eq_top` 📖	mathematical	`Bot.bot` `TwoSidedIdeal` `TwoSidedIdeal.instBot` `Top.top` `TwoSidedIdeal.instTop`	`IsSimpleRing`	—	`TwoSidedIdeal.instNontrivial`
`one_mem_of_ne_bot` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `TwoSidedIdeal.setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`IsSimpleOrder.eq_bot_or_eq_top` `simple`
`one_mem_of_ne_zero_mem` 📖	mathematical	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `TwoSidedIdeal.setLike`	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`one_mem_of_ne_bot`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NonAssocRing.toNonAssocSemiring` `instFunLike`	—	`IsSimpleRing.injective_ringHom_or_subsingleton_codomain` `not_subsingleton`

---

← Back to Index