Documentation Verification Report

Parity

📁 Source: Mathlib/Data/Fin/Parity.lean

Statistics

Metric	Count
Definitions	0
Theorems `even_add_one_iff_odd`, `even_iff`, `even_iff_imp`, `even_iff_mod_of_even`, `even_iff_of_even`, `even_of_odd`, `even_of_val`, `even_succAbove_add_predAbove`, `neg_one_pow_succAbove_add_predAbove`, `not_even_iff_odd_of_even`, `not_odd_iff_even_of_even`, `odd_add_one_iff_even`, `odd_iff`, `odd_iff_imp`, `odd_iff_mod_of_even`, `odd_iff_of_even`, `odd_of_odd`, `odd_of_val`	18
Total	18

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_add_one_iff_odd` 📖	mathematical	—	`Even` `Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`Even.sub_odd` `Even.add_self` `odd_one` `eq_sub_iff_add_eq` `Odd.add_one`
`even_iff` 📖	mathematical	—	`Even` `Odd` `Nat.instSemiring`	—	`Nat.not_even_iff_odd` `imp_iff_not_or` `even_iff_of_even` `even_of_odd` `even_of_val`
`even_iff_imp` 📖	mathematical	—	`Even`	—	`imp_iff_not_or` `Nat.not_even_iff_odd` `even_iff`
`even_iff_mod_of_even` 📖	—	`Even`	—	—	`even_iff_of_even` `Nat.even_iff`
`even_iff_of_even` 📖	—	`Even`	—	—	`val_add_eq_ite` `even_of_val`
`even_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`Even`	—	`LT.lt.ne'` `Nat.even_or_odd` `even_of_val` `Nat.cast_add` `cast_val_eq_self` `natCast_self` `add_zero` `Even.natCast` `Odd.add_odd`
`even_of_val` 📖	—	`Even`	—	—	`LT.lt.ne'` `neZero` `cast_val_eq_self` `Even.natCast`
`even_succAbove_add_predAbove` 📖	mathematical	—	`Even` `succAbove` `predAbove` `Odd` `Nat.instSemiring`	—	`lt_or_ge` `LE.le.trans_lt` `succAbove_of_castSucc_lt` `ne_zero_of_lt` `predAbove_of_castSucc_lt` `succAbove_of_le_castSucc` `predAbove_of_le_castSucc`
`neg_one_pow_succAbove_add_predAbove` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `succAbove` `predAbove`	—	`neg_one_mul` `pow_succ'` `neg_one_pow_congr` `even_succAbove_add_predAbove` `Nat.even_add_one` `Nat.not_even_iff_odd`
`not_even_iff_odd_of_even` 📖	mathematical	`Even`	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`even_iff_of_even` `odd_iff_of_even` `Nat.not_even_iff_odd`
`not_odd_iff_even_of_even` 📖	mathematical	`Even`	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`even_iff_of_even` `odd_iff_of_even` `Nat.not_odd_iff_even`
`odd_add_one_iff_even` 📖	mathematical	—	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Even`	—	`even_two_mul` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `Even.add_one`
`odd_iff` 📖	mathematical	—	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Nat.instSemiring`	—	`Nat.not_even_iff_odd` `imp_iff_not_or` `odd_iff_of_even` `odd_of_odd` `odd_of_val`
`odd_iff_imp` 📖	mathematical	—	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Nat.instSemiring`	—	`imp_iff_not_or` `Nat.not_even_iff_odd` `odd_iff`
`odd_iff_mod_of_even` 📖	mathematical	`Even`	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`odd_iff_of_even` `Nat.odd_iff`
`odd_iff_of_even` 📖	mathematical	`Even`	`Odd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Nat.instSemiring`	—	`coe_ofNat_eq_mod` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `Nat.odd_iff` `Nat.odd_add_one` `Nat.not_odd_iff_even` `Distrib.rightDistribClass` `odd_of_val`
`odd_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`Nat.even_or_odd` `Nat.cast_add` `cast_val_eq_self` `natCast_self` `add_zero` `Odd.natCast` `Even.add_odd` `odd_of_val`
`odd_of_val` 📖	mathematical	`Odd` `Nat.instSemiring`	`CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`neZero` `cast_val_eq_self` `Odd.natCast`

---

← Back to Index