Documentation Verification Report

NonZeroDivisors

📁 Source: Mathlib/RingTheory/OreLocalization/NonZeroDivisors.lean

Statistics

Metric	Count
Definitions `instCommGroupWithZeroNonZeroDivisors`, `instGroupWithZeroNonZeroDivisors`, `inv`, `inv'`	4
Theorems `inv_def`, `inv_zero`, `mul_inv_cancel`, `nontrivial`, `nontrivial_of_nonZeroDivisors`, `nontrivial_of_nonZeroDivisorsLeft`, `nontrivial_of_nonZeroDivisorsRight`	7
Total	11

OreLocalization

Definitions

Name	Category	Theorems
`instCommGroupWithZeroNonZeroDivisors` 📖	CompOp	—
`instGroupWithZeroNonZeroDivisors` 📖	CompOp	—
`inv` 📖	CompOp	—
`inv'` 📖	CompOp	5 math math: `RatFunc.inv_def`, `RatFunc.ofFractionRing_inv`, `mul_inv_cancel`, `inv_zero`, `inv_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_def` 📖	mathematical	—	`OreLocalization` `MonoidWithZero.toMonoid` `nonZeroDivisors` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `inv'` `oreDiv` `instZero` `Submonoid` `MulZeroOneClass.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Monoid.toMulOneClass` `mem_nonZeroDivisors_of_ne_zero`	—	—
`inv_zero` 📖	mathematical	—	`OreLocalization` `MonoidWithZero.toMonoid` `nonZeroDivisors` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `inv'` `instZero`	—	`zero_def` `mem_nonZeroDivisors_of_ne_zero` `inv_def` `zero_oreDiv'`
`mul_inv_cancel` 📖	mathematical	—	`OreLocalization` `MonoidWithZero.toMonoid` `nonZeroDivisors` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `instMul` `inv'` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`ind` `mem_nonZeroDivisors_of_ne_zero` `inv_def` `one_def` `zero_oreDiv'` `mul_inv`
`nontrivial` 📖	mathematical	—	`Nontrivial` `OreLocalization` `MonoidWithZero.toMonoid` `nonZeroDivisors` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero`	—	`nontrivial_of_nonZeroDivisors` `refl` `instReflLe`
`nontrivial_of_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors`	`Nontrivial` `OreLocalization` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulActionWithZero`	—	`nontrivial_of_nonZeroDivisorsLeft` `LE.le.trans` `inf_le_left`
`nontrivial_of_nonZeroDivisorsLeft` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisorsLeft`	`Nontrivial` `OreLocalization` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulActionWithZero`	—	`nontrivial_iff` `one_ne_zero` `NeZero.one` `MulZeroClass.zero_mul`
`nontrivial_of_nonZeroDivisorsRight` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisorsRight`	`Nontrivial` `OreLocalization` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulActionWithZero`	—	`nontrivial_iff` `one_ne_zero` `NeZero.one` `MulZeroClass.mul_zero`

---

← Back to Index