Tuple

📁 Source: Mathlib/Algebra/Group/Fin/Tuple.lean

Statistics

Metric	Count
Definitions	0
Theorems `insertNth_add`, `insertNth_div`, `insertNth_div_same`, `insertNth_mul`, `insertNth_one_right`, `insertNth_sub`, `insertNth_sub_same`, `insertNth_zero_right`, `add_cons`, `cons_add`, `cons_add_cons`, `cons_eq_zero_iff`, `cons_nonzero_iff`, `cons_sub`, `cons_sub_cons`, `cons_zero_zero`, `empty_add_empty`, `empty_sub_empty`, `head_add`, `head_neg`, `head_sub`, `head_zero`, `neg_cons`, `neg_empty`, `smul_cons`, `smul_empty`, `sub_cons`, `tail_add`, `tail_neg`, `tail_sub`, `tail_zero`, `zero_empty`	32
Total	32

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insertNth_add` 📖	mathematical	—	`insertNth` `Pi.instAdd` `succAbove`	—	`insertNth_binop`
`insertNth_div` 📖	mathematical	—	`insertNth` `Pi.instDiv` `succAbove`	—	`insertNth_binop`
`insertNth_div_same` 📖	mathematical	—	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `insertNth` `Pi.mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`div_self'`
`insertNth_mul` 📖	mathematical	—	`insertNth` `Pi.instMul` `succAbove`	—	`insertNth_binop`
`insertNth_one_right` 📖	mathematical	—	`insertNth` `Pi.instOne` `succAbove` `Pi.mulSingle`	—	`insertNth_eq_iff` `Pi.mulSingle_eq_same` `Pi.mulSingle_eq_of_ne`
`insertNth_sub` 📖	mathematical	—	`insertNth` `Pi.instSub` `succAbove`	—	`insertNth_binop`
`insertNth_sub_same` 📖	mathematical	—	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `insertNth` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`insertNth_sub` `insertNth_zero_right` `sub_self`
`insertNth_zero_right` 📖	mathematical	—	`insertNth` `Pi.instZero` `succAbove` `Pi.single`	—	`insertNth_eq_iff` `Pi.single_eq_same` `Pi.single_eq_of_ne` `succAbove_ne`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_cons` 📖	mathematical	—	`Pi.instAdd` `vecCons` `vecHead` `vecTail`	—	`cons_val_succ`
`cons_add` 📖	mathematical	—	`Pi.instAdd` `vecCons` `vecHead` `vecTail`	—	`cons_val_succ`
`cons_add_cons` 📖	mathematical	—	`Pi.instAdd` `vecCons`	—	`add_cons` `tail_cons`
`cons_eq_zero_iff` 📖	mathematical	—	`vecCons` `Pi.instZero`	—	`cons_zero_zero`
`cons_nonzero_iff` 📖	—	—	—	—	`not_and_or` `cons_eq_zero_iff`
`cons_sub` 📖	mathematical	—	`Pi.instSub` `vecCons` `vecHead` `vecTail`	—	`cons_val_succ`
`cons_sub_cons` 📖	mathematical	—	`Pi.instSub` `vecCons`	—	`sub_cons` `tail_cons`
`cons_zero_zero` 📖	mathematical	—	`vecCons` `Pi.instZero`	—	`cons_val_succ`
`empty_add_empty` 📖	mathematical	—	`Pi.instAdd` `vecEmpty`	—	`empty_eq`
`empty_sub_empty` 📖	mathematical	—	`Pi.instSub` `vecEmpty`	—	`empty_eq`
`head_add` 📖	mathematical	—	`vecHead` `Pi.instAdd`	—	—
`head_neg` 📖	mathematical	—	`vecHead` `Pi.instNeg`	—	—
`head_sub` 📖	mathematical	—	`vecHead` `Pi.instSub`	—	—
`head_zero` 📖	mathematical	—	`vecHead` `Pi.instZero`	—	—
`neg_cons` 📖	mathematical	—	`Pi.instNeg` `vecCons`	—	`cons_val_succ`
`neg_empty` 📖	mathematical	—	`Pi.instNeg` `vecEmpty`	—	`empty_eq`
`smul_cons` 📖	mathematical	—	`Pi.instSMul` `vecCons`	—	`cons_val_succ`
`smul_empty` 📖	mathematical	—	`Pi.instSMul` `vecEmpty`	—	`empty_eq`
`sub_cons` 📖	mathematical	—	`Pi.instSub` `vecCons` `vecHead` `vecTail`	—	`cons_val_succ`
`tail_add` 📖	mathematical	—	`vecTail` `Pi.instAdd`	—	—
`tail_neg` 📖	mathematical	—	`vecTail` `Pi.instNeg`	—	—
`tail_sub` 📖	mathematical	—	`vecTail` `Pi.instSub`	—	—
`tail_zero` 📖	mathematical	—	`vecTail` `Pi.instZero`	—	—
`zero_empty` 📖	mathematical	—	`Pi.instZero` `vecEmpty`	—	`empty_eq`

---

← Back to Index