Field

📁 Source: Mathlib/SetTheory/Nimber/Field.lean

Statistics

Metric	Count
Definitions `instCommRing`, `instField`, `instInv`, `instMul`, `instMulZeroClass`, `invAux`, `invSet`, `mul`	8
Theorems `add_mul`, `cons_mem_invSet`, `exists_of_lt_mul`, `instCharPOfNatNat`, `instIsCancelMulZero`, `instIsDomain`, `instNoZeroDivisors`, `instSmallElemInvSet`, `invAux_mem_invSet_of_lt`, `invAux_ne_zero`, `invAux_notMem_invSet`, `invSet_recOn`, `inv_eq_invAux`, `mem_invSet_of_lt_invAux`, `mul_add`, `mul_assoc`, `mul_comm`, `mul_def`, `mul_invAux_cancel`, `mul_le_of_forall_ne`, `mul_one`, `one_mul`, `zero_mem_invSet`	23
Total	31

Nimber

Definitions

Name	Category	Theorems
`instCommRing` 📖	CompOp	1 math math: `instIsDomain`
`instField` 📖	CompOp	—
`instInv` 📖	CompOp	1 math math: `inv_eq_invAux`
`instMul` 📖	CompOp	12 math math: `instNoZeroDivisors`, `mul_le_of_forall_ne`, `mul_assoc`, `mul_add`, `cons_mem_invSet`, `mul_invAux_cancel`, `one_mul`, `mul_def`, `add_mul`, `mul_comm`, `instIsCancelMulZero`, `mul_one`
`instMulZeroClass` 📖	CompOp	—
`invAux` 📖	CompOp	5 math math: `invAux_notMem_invSet`, `cons_mem_invSet`, `mul_invAux_cancel`, `inv_eq_invAux`, `invAux_mem_invSet_of_lt`
`invSet` 📖	CompOp	5 math math: `instSmallElemInvSet`, `zero_mem_invSet`, `invAux_notMem_invSet`, `invAux_mem_invSet_of_lt`, `mem_invSet_of_lt_invAux`
`mul` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mul` 📖	mathematical	—	`Nimber` `instMul` `instAdd`	—	`mul_comm` `mul_add`
`cons_mem_invSet` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership` `invSet`	`instMul` `invAux` `instAdd` `instOneNimber`	—	`invSet.eq_1` `Set.mem_sInter`
`exists_of_lt_mul` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `instMul`	`instAdd`	—	`notMem_of_lt_csInf'` `mul_def` `Set.notMem_compl_iff`
`instCharPOfNatNat` 📖	mathematical	—	`CharP` `Nimber` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOne`	—	`CharTwo.of_one_ne_zero_of_two_eq_zero` `one_ne_zero` `instNeZeroOne` `Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `add_self`
`instIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `Nimber` `instMul` `instZeroNimber`	—	`add_eq_zero` `mul_eq_zero` `instNoZeroDivisors` `mul_add` `add_mul`
`instIsDomain` 📖	mathematical	—	`IsDomain` `Nimber` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`instIsCancelMulZero`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `Nimber` `instMul` `instZeroNimber`	—	`pos_iff_ne_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `zero_add`
`instSmallElemInvSet` 📖	mathematical	—	`Small` `Set.Elem` `Nimber` `invSet`	—	`small_subset` `OrderIso.symm_apply_apply` `small_range` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`invAux_mem_invSet_of_lt` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	`Set` `Set.instMembership` `invSet` `invAux`	—	`cons_mem_invSet` `zero_mem_invSet` `mul_one` `add_zero` `MulZeroClass.mul_zero`
`invAux_ne_zero` 📖	—	—	—	—	`invAux.eq_1` `csInf_mem` `instWellFoundedLT` `zero_mem_invSet`
`invAux_notMem_invSet` 📖	mathematical	—	`Nimber` `Set` `Set.instMembership` `invSet` `invAux`	—	`invAux.eq_1` `csInf_mem` `instWellFoundedLT`
`invSet_recOn` 📖	—	`Nimber` `instZeroNimber` `instMul` `invAux` `instAdd` `instOneNimber` `Set` `Set.instMembership` `invSet`	—	—	`invSet.eq_1` `Set.sInter_subset_of_mem`
`inv_eq_invAux` 📖	mathematical	—	`Nimber` `instInv` `invAux`	—	—
`mem_invSet_of_lt_invAux` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `invAux`	`Set` `Set.instMembership` `invSet`	—	`notMem_of_lt_csInf` `invAux.eq_1` `bot_mem_lowerBounds` `Set.notMem_compl_iff`
`mul_add` 📖	mathematical	—	`Nimber` `instMul` `instAdd`	—	—
`mul_assoc` 📖	mathematical	—	`Nimber` `instMul`	—	—
`mul_comm` 📖	mathematical	—	`Nimber` `instMul`	—	—
`mul_def` 📖	mathematical	—	`Nimber` `instMul` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Compl.compl` `Set` `Set.instCompl` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `instAdd`	—	`mul.eq_1`
`mul_invAux_cancel` 📖	mathematical	—	`Nimber` `instMul` `invAux` `instOneNimber`	—	—
`mul_le_of_forall_ne` 📖	mathematical	—	`Nimber` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `instMul`	—	`exists_of_lt_mul`
`mul_one` 📖	mathematical	—	`Nimber` `instMul` `instOneNimber`	—	`mul_comm` `one_mul`
`one_mul` 📖	mathematical	—	`Nimber` `instMul` `instOneNimber`	—	`le_antisymm` `mul_le_of_forall_ne` `lt_one_iff_zero` `MulZeroClass.zero_mul` `add_zero` `zero_add` `LT.lt.ne` `Eq.not_lt` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `one_ne_zero` `instNeZeroOne`
`zero_mem_invSet` 📖	mathematical	—	`Nimber` `Set` `Set.instMembership` `invSet` `instZeroNimber`	—	`invSet.eq_1` `Set.mem_sInter`

---

← Back to Index