Documentation

Mathlib.Algebra.Group.Nat.Even

IsSquare and Even for natural numbers #

Parity #

theorem Nat.even_iff {n : } :
Even n n % 2 = 0

IsSquare can be decided on by checking against the square root.

Equations
    theorem Nat.not_even_iff {n : } :
    ¬Even n n % 2 = 1
    @[simp]
    theorem Nat.two_dvd_ne_zero {n : } :
    ¬2 n n % 2 = 1
    @[simp]
    theorem Nat.even_add {m n : } :
    Even (m + n) (Even m Even n)
    theorem Nat.even_add_one {n : } :
    Even (n + 1) ¬Even n
    theorem Nat.succ_mod_two_eq_zero_iff {m : } :
    (m + 1) % 2 = 0 m % 2 = 1
    theorem Nat.succ_mod_two_eq_one_iff {m : } :
    (m + 1) % 2 = 1 m % 2 = 0
    theorem Nat.two_not_dvd_two_mul_sub_one {n : } :
    0 < n¬2 2 * n - 1
    theorem Nat.even_sub {m n : } (h : n m) :
    Even (m - n) (Even m Even n)
    theorem Nat.even_mul {m n : } :
    Even (m * n) Even m Even n
    theorem Nat.even_pow {m n : } :
    Even (m ^ n) Even m n 0

    If m and n are natural numbers, then the natural number m^n is even if and only if m is even and n is positive.

    theorem Nat.even_pow' {m n : } (h : n 0) :
    Even (m ^ n) Even m
    theorem Nat.even_mul_succ_self (n : ) :
    Even (n * (n + 1))
    theorem Nat.even_mul_pred_self (n : ) :
    Even (n * (n - 1))
    theorem Nat.two_mul_div_two_of_even {n : } :
    Even n2 * (n / 2) = n
    theorem Nat.div_two_mul_two_of_even {n : } :
    Even nn / 2 * 2 = n
    theorem Nat.one_lt_of_ne_zero_of_even {n : } (h0 : n 0) (hn : Even n) :
    1 < n
    theorem Nat.add_one_lt_of_even {m n : } (hn : Even n) (hm : Even m) (hnm : n < m) :
    n + 1 < m