Documentation Verification Report

Arithmetic

📁 Source: Mathlib/Order/Types/Arithmetic.lean

Statistics

Metric	Count
Definitions `eta`, `instAdd`, `instAddMonoid`, `instHAdd`, `instHMul`, `instMonoid`, `instMul`, `instOfNat`, `termη`, `termθ`, `theta`	11
Theorems `instLeftDistribClass`, `instZeroLEOneClass`, `type_lex_prod`, `type_lex_sum`	4
Total	15

OrderType

Definitions

Name	Category	Theorems
`eta` 📖	CompOp	—
`instAdd` 📖	CompOp	1 math math: `instLeftDistribClass`
`instAddMonoid` 📖	CompOp	—
`instHAdd` 📖	CompOp	1 math math: `type_lex_sum`
`instHMul` 📖	CompOp	1 math math: `type_lex_prod`
`instMonoid` 📖	CompOp	—
`instMul` 📖	CompOp	1 math math: `instLeftDistribClass`
`instOfNat` 📖	CompOp	—
`termη` 📖	CompOp	—
`termθ` 📖	CompOp	—
`theta` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLeftDistribClass` 📖	mathematical	—	`LeftDistribClass` `OrderType` `instMul` `instAdd`	—	`inductionOn₃` `OrderIso.type_congr`
`instZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `OrderType` `instZero` `instOne` `Preorder.toLE` `instPreorder`	—	`zero_le`
`type_lex_prod` 📖	mathematical	—	`type` `Lex` `Prod.Lex.instLinearOrder` `OrderType` `instHMul`	—	`liftOn₂_type`
`type_lex_sum` 📖	mathematical	—	`type` `Lex` `Sum.Lex.linearOrder` `OrderType` `instHAdd`	—	`liftOn₂_type`

---

← Back to Index