Theorems · Definition · real analysis
Function.Even
{α : Type u_1} → {β : Type u_2} → [Neg α] → (α → β) → PropA function f is _even_ if it satisfies f (-x) = f x for all x.
- Defined in
- Mathlib.Algebra.Group.EvenFunction
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Neg
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by36
Results whose statement or proof uses this declaration.
- DirichletCharacter.Even.to_funstatement · cited by 3
- ZMod.LFunction_def_evenstatement and proof · cited by 3
- tsum_int_eq_zero_add_two_mul_tsum_pnatstatement and proof · cited by 2
- ZMod.completedLFunction_def_evenstatement and proof · cited by 2
- Function.locallyFinsuppWithin.logCounting_evenstatement · cited by 1
- Summable.tendsto_zero_of_even_summable_symmetricIccstatement and proof · cited by 1
- EisensteinSeries.e2Summand_evenstatement · cited by 1
- Function.Odd.mul_evenstatement and proof · cited by 1
- ZMod.LFunction_eq_completed_div_gammaFactor_evenstatement and proof · cited by 1
- ZMod.LFunction_neg_two_mul_nat_add_onestatement and proof · cited by 1
- Function.Even.addstatement and proof · cited by 1
- Function.Even.conststatement · cited by 1