Theorems · Theorem · number theory
Even.two_dvd
∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → 2 ∣ aAlias of the forward direction of even_iff_two_dvd.
- Defined in
- Mathlib.Algebra.Ring.Parity
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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
- even_iff_two_dvdproof · cited by 25
Cited by15
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- Even.trans_dvdproof · cited by 1
- NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvdproof · cited by 1
- Nat.two_mul_smallSchroder_succproof · cited by 1
- CoxeterSystem.prod_alternatingWord_eq_mul_powproof · cited by 1
- LucasLehmer.X.pow_ωproof · cited by 1
- Algebra.discr_powerBasis_eq_prod''proof · cited by 1
- Nat.exists_eq_two_pow_mul_oddproof · cited by 1
- CharTwo.of_one_ne_zero_of_two_eq_zeroproof · cited by 0
- Nat.totient_two_mul_of_evenproof · cited by 0
- SimpleGraph.mul_card_edgeFinset_turanGraph_leproof · cited by 0
- ZMod.isCyclic_units_iffproof · cited by 0