Mathlib Map

Theorems · Theorem · number theory

even_two_mul

∀ {α : Type u_2} [inst : Semiring α] (a : α), Even (2 * a)
Defined in
Mathlib.Algebra.Ring.Parity
Cited by
102 results in Mathlib
Foundations
Depth 20 from the axioms, rests on 199 definitions · uses propext
Assumes
Semiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Orientation.oangle_self · cited by 17Orientation.oangle_selfFunction.hasTemperateGrowth_one_add_norm_sq_rpow · cited by 9Function.hasTemperateGrow…hasFDerivAt_jacobiTheta₂ · cited by 4hasFDerivAt_jacobiTheta₂AkraBazziRecurrence.eventually_bi_mul_le_r · cited by 4AkraBazziRecurrence.event…IsCyclotomicExtension.discr_prime_pow_ne_two · cited by 4IsCyclotomicExtension.dis…ProbabilityTheory.IsGaussian.memLp_id · cited by 4IsGaussian.memLp_idOrthonormalBasis.sum_sq_norm_inner_right · cited by 3OrthonormalBasis.sum_sq_n…Complex.norm_exp_sub_one_sub_id_le · cited by 3Complex.norm_exp_sub_one_…ProbabilityTheory.gaussianReal_map_linearMap · cited by 3ProbabilityTheory.gaussia…preNormEDS'_odd · cited by 3preNormEDS'_oddOdd.pow_neg_iff · cited by 3Odd.pow_neg_iffOdd.zpow_neg_iff · cited by 3Odd.zpow_neg_iffTemperedDistribution.besselPotential_besselPotential_apply · cited by 3TemperedDistribution.bess…ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le · cited by 2Fernique.lintegral_closed…SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj · cited by 2SimpleGraph.lapMatrix_toL…Semiring · cited by 13802SemiringEven · cited by 444Eventwo_mul · cited by 232two_muleven_two_mulCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Semiringstatement and proof · cited by 13,802
  • Evenstatement · cited by 444
  • two_mulproof · cited by 232

Cited by102

Results whose statement or proof uses this declaration.