Documentation Verification Report

Translate

📁 Source: Mathlib/Algebra/Group/Translate.lean

Statistics

Metric	Count
Definitions `translate`, `termτ`	2
Theorems `comp_translate`, `sum_translate`, `support_translate`, `translate_add`, `translate_add'`, `translate_add_right`, `translate_apply`, `translate_comm`, `translate_eq_domAddActMk_vadd`, `translate_neg_right`, `translate_prod_right`, `translate_smul_right`, `translate_sub_right`, `translate_sum_right`, `translate_translate`, `translate_zero`, `translate_zero_right`	17
Total	19

(root)

Definitions

Name	Category	Theorems
`translate` 📖	CompOp	17 math math: `translate_prod_right`, `translate_sum_right`, `translate_zero_right`, `translate_comm`, `translate_add_right`, `translate_eq_domAddActMk_vadd`, `translate_sub_right`, `translate_smul_right`, `comp_translate`, `translate_zero`, `translate_translate`, `translate_apply`, `support_translate`, `translate_neg_right`, `translate_add'`, `sum_translate`, `translate_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_translate` 📖	mathematical	—	`translate`	—	—
`sum_translate` 📖	mathematical	—	`Finset.sum` `Finset.univ` `translate`	—	`Fintype.sum_equiv`
`support_translate` 📖	mathematical	—	`Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `translate` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Set.ext` `sub_eq_neg_add`
`translate_add` 📖	mathematical	—	`translate` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`sub_sub`
`translate_add'` 📖	mathematical	—	`translate` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `translate_add`
`translate_add_right` 📖	mathematical	—	`translate` `Pi.instAdd`	—	—
`translate_apply` 📖	mathematical	—	`translate` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`translate_comm` 📖	mathematical	—	`translate`	—	`translate_add` `translate_add'`
`translate_eq_domAddActMk_vadd` 📖	mathematical	—	`translate` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `DomAddAct.instVAddForall` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_eq_neg_add` `Equiv.symm_apply_apply`
`translate_neg_right` 📖	mathematical	—	`translate` `Pi.instNeg`	—	—
`translate_prod_right` 📖	mathematical	—	`translate` `Finset.prod` `Pi.commMonoid`	—	`Finset.prod_apply` `Finset.prod_congr`
`translate_smul_right` 📖	mathematical	—	`translate` `Function.hasSMul`	—	—
`translate_sub_right` 📖	mathematical	—	`translate` `Pi.instSub`	—	—
`translate_sum_right` 📖	mathematical	—	`translate` `Finset.sum` `Pi.addCommMonoid`	—	`Finset.sum_apply` `Finset.sum_congr`
`translate_translate` 📖	mathematical	—	`translate` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`sub_sub`
`translate_zero` 📖	mathematical	—	`translate` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_zero`
`translate_zero_right` 📖	mathematical	—	`translate` `Pi.instZero`	—	—

translate

Definitions

Name	Category	Theorems
`termτ` 📖	CompOp	—

---

← Back to Index