Even

Statistics

Metric	Count
Definitions `instDecidablePredEven`, `instDecidablePredIsSquare`	2
Theorems `add_one_lt_of_even`, `div_two_mul_two_of_even`, `even_add`, `even_add_one`, `even_iff`, `even_mul`, `even_mul_pred_self`, `even_mul_succ_self`, `even_pow`, `even_pow'`, `even_sub`, `not_even_iff`, `not_even_one`, `one_lt_of_ne_zero_of_even`, `succ_mod_two_eq_one_iff`, `succ_mod_two_eq_zero_iff`, `two_dvd_ne_zero`, `two_mul_div_two_of_even`, `two_not_dvd_two_mul_add_one`, `two_not_dvd_two_mul_sub_one`	20
Total	22

Name	Category	Theorems
`instDecidablePredEven` 📖	CompOp	29 math math: `neg_one_pow_eq_ite`, `IsCyclotomicExtension.Rat.torsionOrder_eq`, `WeierstrassCurve.coeff_preΨ'`, `geom_sum_alternating_of_le_neg_one`, `Fin.sum_neg_one_pow`, `WeierstrassCurve.leadingCoeff_preΨ'`, `hyperoperation_ge_four_zero`, `WeierstrassCurve.ΨSq_ofNat`, `WeierstrassCurve.Ψ_ofNat`, `preNormEDS'_odd`, `schnirelmannDensity_setOf_even`, `CoxeterSystem.getElem_alternatingWord`, `AlternatingGroup.card_of_cycleType`, `WeierstrassCurve.Φ_ofNat`, `WeierstrassCurve.preΨ'_odd`, `geom_sum_alternating_of_lt_neg_one`, `neg_one_geom_sum`, `CoxeterSystem.prod_alternatingWord_eq_mul_pow`, `HomologicalComplex.alternatingConst_d`, `CoxeterSystem.listTake_alternatingWord`, `CoxeterSystem.alternatingWord_succ'`, `WeierstrassCurve.natDegree_preΨ'`, `CharTwo.natCast_eq_ite`, `normEDS_ofNat`, `WeierstrassCurve.natDegree_preΨ'_le`, `Polynomial.coeff_hermite`, `List.IsChain.two_mul_count_bool_eq_ite`, `AlternatingGroup.map_subtype_of_cycleType`, `AlternatingGroup.card_of_cycleType_mul_eq`
`instDecidablePredIsSquare` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one_lt_of_even` 📖	—	`Even`	—	—	—
`div_two_mul_two_of_even` 📖	—	`Even`	—	—	`even_iff_exists_two_nsmul`
`even_add` 📖	mathematical	—	`Even`	—	—
`even_add_one` 📖	mathematical	—	`Even`	—	—
`even_iff` 📖	mathematical	—	`Even`	—	—
`even_mul` 📖	mathematical	—	`Even`	—	`mul_one` `one_mul`
`even_mul_pred_self` 📖	mathematical	—	`Even`	—	—
`even_mul_succ_self` 📖	mathematical	—	`Even`	—	—
`even_pow` 📖	mathematical	—	`Even` `Monoid.toPow` `instMonoid`	—	—
`even_pow'` 📖	mathematical	—	`Even` `Monoid.toPow` `instMonoid`	—	—
`even_sub` 📖	mathematical	—	`Even`	—	—
`not_even_iff` 📖	mathematical	—	`Even`	—	—
`not_even_one` 📖	mathematical	—	`Even`	—	—
`one_lt_of_ne_zero_of_even` 📖	—	`Even`	—	—	—
`succ_mod_two_eq_one_iff` 📖	—	—	—	—	—
`succ_mod_two_eq_zero_iff` 📖	—	—	—	—	—
`two_dvd_ne_zero` 📖	—	—	—	—	—
`two_mul_div_two_of_even` 📖	—	`Even`	—	—	`even_iff_exists_two_nsmul`
`two_not_dvd_two_mul_add_one` 📖	—	—	—	—	—
`two_not_dvd_two_mul_sub_one` 📖	—	—	—	—	—

---