Theorems · Definition · real analysis
Function.Odd
{α : Type u_1} → {β : Type u_2} → [Neg α] → [Neg β] → (α → β) → PropA function f is _odd_ if it satisfies f (-x) = -f x for all x.
- Defined in
- Mathlib.Algebra.Group.EvenFunction
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
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 by38
Results whose statement or proof uses this declaration.
- IsEllipticNet.atom_neg_leftstatement and proof · cited by 4
- IsEllipticNet.atom_abs_leftstatement and proof · cited by 3
- DirichletCharacter.Odd.to_funstatement · cited by 3
- Function.Odd.sum_eq_zerostatement and proof · cited by 3
- IsEllipticNet.neg_atomstatement and proof · cited by 3
- ZMod.LFunction_def_oddstatement and proof · cited by 2
- Function.Odd.finsetSum_eq_zerostatement and proof · cited by 2
- ZMod.dft_odd_iffstatement and proof · cited by 1
- Function.Odd.map_zerostatement and proof · cited by 1
- Function.Odd.mul_evenstatement and proof · cited by 1
- ZMod.LFunction_eq_completed_div_gammaFactor_oddstatement and proof · cited by 1
- IsEllipticNet.atomRel_neg₁statement and proof · cited by 1