Documentation Verification Report

EvenFunction

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

Statistics

Metric	Count
Definitions	0
Theorems `add`, `comp_odd`, `const`, `const_smul`, `left_comp`, `mul_even`, `mul_odd`, `smul_even`, `smul_odd`, `zero`, `add`, `comp_odd`, `const_smul`, `finset_sum_eq_zero`, `map_zero`, `mul_even`, `mul_odd`, `smul_even`, `smul_odd`, `sum_eq_zero`, `zero`, `zero_of_even_and_odd`	22
Total	22

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_of_even_and_odd` 📖	mathematical	`Even` `Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Pi.zero_apply` `neg_eq_self`

Function.Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Function.Even`	`Function.Even` `Pi.instAdd`	—	—
`comp_odd` 📖	mathematical	`Function.Even` `Function.Odd`	`Function.Even`	—	—
`const` 📖	mathematical	—	`Function.Even`	—	—
`const_smul` 📖	mathematical	`Function.Even`	`Function.Even` `Function.hasSMul`	—	—
`left_comp` 📖	mathematical	`Function.Even`	`Function.Even`	—	—
`mul_even` 📖	mathematical	`Function.Even`	`Function.Even` `Pi.instMul`	—	—
`mul_odd` 📖	mathematical	`Function.Even` `Function.Odd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	`Function.Odd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Pi.instMul`	—	`mul_neg`
`smul_even` 📖	mathematical	`Function.Even`	`Function.Even` `Pi.smul'`	—	—
`smul_odd` 📖	mathematical	`Function.Even` `Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_neg`
`zero` 📖	mathematical	—	`Function.Even`	—	`const`

Function.Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubtractionCommMonoid.toAddCommMonoid`	—	`neg_add`
`comp_odd` 📖	mathematical	`Function.Odd`	`Function.Odd`	—	—
`const_smul` 📖	mathematical	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_neg`
`finset_sum_eq_zero` 📖	mathematical	`Function.Odd` `InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finset.map` `Equiv.toEmbedding` `Equiv.neg`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.sum_congr` `Finset.sum_neg_distrib` `Finset.sum_map`
`map_zero` 📖	mathematical	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_zero`
`mul_even` 📖	mathematical	`Function.Odd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Function.Even`	`Function.Odd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Pi.instMul`	—	`neg_mul`
`mul_odd` 📖	mathematical	`Function.Odd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	`Function.Even` `Pi.instMul`	—	`mul_neg` `neg_mul` `neg_neg`
`smul_even` 📖	mathematical	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Function.Even`	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`neg_smul`
`smul_odd` 📖	mathematical	`Function.Odd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`Function.Even` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_neg` `neg_smul` `neg_neg`
`sum_eq_zero` 📖	mathematical	`Function.Odd` `InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`finset_sum_eq_zero` `Finset.map_univ_equiv`
`zero` 📖	mathematical	—	`Function.Odd` `NegZeroClass.toNeg` `NegZeroClass.toZero`	—	`neg_zero`

---

← Back to Index