Documentation Verification Report

Even

📁 Source: Mathlib/Algebra/Group/Int/Even.lean

Statistics

Metric	Count
Definitions `instDecidablePredEven`, `instDecidablePredIsSquare`	2
Theorems `ediv_two_mul_two_of_even`, `emod_two_ne_one`, `emod_two_ne_zero`, `even_add`, `even_add_one`, `even_coe_nat`, `even_iff`, `even_mul`, `even_pow`, `even_pow'`, `even_sub`, `even_sub_one`, `isSquare_sign_iff`, `not_even_iff`, `not_even_one`, `one_emod_two`, `two_dvd_ne_zero`, `two_mul_ediv_two_of_even`, `two_not_dvd_two_mul_add_one`	19
Total	21

Int

Definitions

Name	Category	Theorems
`instDecidablePredEven` 📖	CompOp	13 math math: `Polynomial.Chebyshev.U_eval_zero`, `WeierstrassCurve.ΨSq_odd`, `Polynomial.Chebyshev.T_eval_zero`, `WeierstrassCurve.preΨ_odd`, `WeierstrassCurve.coeff_preΨ`, `WeierstrassCurve.leadingCoeff_preΨ`, `fib_neg`, `neg_one_zpow_eq_ite`, `WeierstrassCurve.natDegree_preΨ_le`, `preNormEDS_mul_complEDS₂`, `preNormEDS_odd`, `WeierstrassCurve.Ψ_odd`, `WeierstrassCurve.natDegree_preΨ`
`instDecidablePredIsSquare` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ediv_two_mul_two_of_even` 📖	—	`Even`	—	—	—
`emod_two_ne_one` 📖	—	—	—	—	—
`emod_two_ne_zero` 📖	—	—	—	—	—
`even_add` 📖	mathematical	—	`Even`	—	—
`even_add_one` 📖	mathematical	—	`Even`	—	—
`even_coe_nat` 📖	mathematical	—	`Even`	—	`even_iff` `Nat.even_iff`
`even_iff` 📖	mathematical	—	`Even`	—	—
`even_mul` 📖	mathematical	—	`Even`	—	`emod_two_eq_zero_or_one` `mul_one` `one_mul`
`even_pow` 📖	mathematical	—	`Even` `Monoid.toNatPow` `instMonoid`	—	—
`even_pow'` 📖	mathematical	—	`Even` `Monoid.toNatPow` `instMonoid`	—	—
`even_sub` 📖	mathematical	—	`Even`	—	—
`even_sub_one` 📖	mathematical	—	`Even`	—	—
`isSquare_sign_iff` 📖	mathematical	—	`IsSquare`	—	`induction_on` `neg_add'`
`not_even_iff` 📖	mathematical	—	`Even`	—	—
`not_even_one` 📖	mathematical	—	`Even`	—	—
`one_emod_two` 📖	—	—	—	—	—
`two_dvd_ne_zero` 📖	—	—	—	—	—
`two_mul_ediv_two_of_even` 📖	—	`Even`	—	—	—
`two_not_dvd_two_mul_add_one` 📖	—	—	—	—	—

---

← Back to Index