Lemmas

📁 Source: Batteries/Data/Nat/Lemmas.lean

Statistics

Metric	Count
Definitions `lt_sum_ge`, `sum_trichotomy`	2
Theorems `add_mul_lt_mul_of_lt_of_lt`, `casesAuxOn_succ`, `casesAuxOn_zero`, `casesDiagOn_succ_succ`, `casesDiagOn_succ_zero`, `casesDiagOn_zero_succ`, `casesDiagOn_zero_zero`, `mul_add_lt_mul_of_lt_of_lt`, `ofBits_lt_two_pow`, `ofBits_succ`, `ofBits_testBit`, `ofBits_zero`, `recAuxOn_succ`, `recAuxOn_zero`, `recAux_succ`, `recAux_zero`, `recDiagAux_succ_succ`, `recDiagAux_zero_left`, `recDiagAux_zero_right`, `recDiagOn_succ_succ`, `recDiagOn_succ_zero`, `recDiagOn_zero_succ`, `recDiagOn_zero_zero`, `recDiag_succ_succ`, `recDiag_succ_zero`, `recDiag_zero_succ`, `recDiag_zero_zero`, `strongRecOn_eq`, `strongRec_eq`, `sum_append`, `testBit_ofBits`, `testBit_ofBits_ge`, `testBit_ofBits_lt`	33
Total	35

Nat

Definitions

Name	Category	Theorems
`lt_sum_ge` 📖	CompOp	—
`sum_trichotomy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mul_lt_mul_of_lt_of_lt` 📖	—	—	—	—	`mul_add_lt_mul_of_lt_of_lt`
`casesAuxOn_succ` 📖	—	—	—	—	—
`casesAuxOn_zero` 📖	—	—	—	—	—
`casesDiagOn_succ_succ` 📖	mathematical	—	`casesDiagOn`	—	—
`casesDiagOn_succ_zero` 📖	mathematical	—	`casesDiagOn`	—	—
`casesDiagOn_zero_succ` 📖	mathematical	—	`casesDiagOn`	—	—
`casesDiagOn_zero_zero` 📖	mathematical	—	`casesDiagOn`	—	—
`mul_add_lt_mul_of_lt_of_lt` 📖	—	—	—	—	—
`ofBits_lt_two_pow` 📖	mathematical	—	`ofBits`	—	`ofBits_succ`
`ofBits_succ` 📖	mathematical	—	`ofBits`	—	—
`ofBits_testBit` 📖	mathematical	—	`ofBits`	—	`testBit_ofBits`
`ofBits_zero` 📖	mathematical	—	`ofBits`	—	—
`recAuxOn_succ` 📖	mathematical	—	`recAuxOn`	—	—
`recAuxOn_zero` 📖	mathematical	—	`recAuxOn`	—	—
`recAux_succ` 📖	—	—	—	—	—
`recAux_zero` 📖	—	—	—	—	—
`recDiagAux_succ_succ` 📖	mathematical	—	`recDiagAux`	—	—
`recDiagAux_zero_left` 📖	mathematical	—	`recDiagAux`	—	—
`recDiagAux_zero_right` 📖	mathematical	—	`recDiagAux`	—	—
`recDiagOn_succ_succ` 📖	mathematical	—	`recDiagOn`	—	—
`recDiagOn_succ_zero` 📖	mathematical	—	`recDiagOn`	—	`recDiag_succ_zero`
`recDiagOn_zero_succ` 📖	mathematical	—	`recDiagOn`	—	`recDiag_zero_succ`
`recDiagOn_zero_zero` 📖	mathematical	—	`recDiagOn`	—	—
`recDiag_succ_succ` 📖	mathematical	—	`recDiag`	—	—
`recDiag_succ_zero` 📖	mathematical	—	`recDiag`	—	—
`recDiag_zero_succ` 📖	mathematical	—	`recDiag`	—	`recDiagAux_zero_left`
`recDiag_zero_zero` 📖	mathematical	—	`recDiag`	—	—
`strongRecOn_eq` 📖	—	—	—	—	—
`strongRec_eq` 📖	mathematical	—	`strongRec`	—	`strongRec.eq_def`
`sum_append` 📖	—	—	—	—	—
`testBit_ofBits` 📖	mathematical	—	`ofBits`	—	`testBit_ofBits_lt` `testBit_ofBits_ge`
`testBit_ofBits_ge` 📖	mathematical	—	`ofBits`	—	`ofBits_lt_two_pow`
`testBit_ofBits_lt` 📖	mathematical	—	`ofBits`	—	`ofBits_succ`

---

← Back to Index