Loogle!

Result

Found 330 declarations mentioning Odd. Of these, only the first 200 are shown.

• Odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] (a : α) : Prop
• Nat.instDecidablePredOdd 📋 Mathlib.Algebra.Ring.Parity
  : DecidablePred Odd
• Nat.not_odd_zero 📋 Mathlib.Algebra.Ring.Parity
  : ¬Odd 0
• Nat.even_or_odd 📋 Mathlib.Algebra.Ring.Parity
  (n : ℕ) : Even n ∨ Odd n
• Nat.even_xor_odd 📋 Mathlib.Algebra.Ring.Parity
  (n : ℕ) : Xor (Even n) (Odd n)
• Nat.not_even_iff_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : ¬Even n ↔ Odd n
• Nat.not_odd_iff_even 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : ¬Odd n ↔ Even n
• Odd.not_two_dvd_nat 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : ¬2 ∣ n
• Nat.ne_of_odd_add 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : Odd (m + n)) : m ≠ n
• Nat.Odd.of_mul_left 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : Odd (m * n)) : Odd m
• Nat.Odd.of_mul_right 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : Odd (m * n)) : Odd n
• Function.Involutive.iterate_odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_4} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hn : Odd n) : f^[n] = f
• odd_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] : Odd 1
• Odd.tsub_odd 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)
• Nat.Odd.sub_odd 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)
• Nat.odd_add_one 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : Odd (n + 1) ↔ ¬Odd n
• Odd.natCast 📋 Mathlib.Algebra.Ring.Parity
  {R : Type u_4} [Semiring R] {n : ℕ} (hn : Odd n) : Odd ↑n
• Nat.even_add' 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} : Even (m + n) ↔ (Odd m ↔ Odd n)
• Nat.odd_add 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} : Odd (m + n) ↔ (Odd m ↔ Even n)
• Nat.odd_add' 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} : Odd (m + n) ↔ (Odd n ↔ Even m)
• Nat.odd_mul 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} : Odd (m * n) ↔ Odd m ∧ Odd n
• Nat.odd_iff 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : Odd n ↔ n % 2 = 1
• Function.Involutive.iterate_eq_self 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_4} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n
• Nat.not_odd_iff 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : ¬Odd n ↔ n % 2 = 0
• Nat.Even.sub_odd 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n)
• Nat.Odd.sub_even 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : n ≤ m) (hm : Odd m) (hn : Even n) : Odd (m - n)
• Odd.pow 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} {n : ℕ} (ha : Odd a) : Odd (a ^ n)
• Nat.even_sub' 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n)
• Nat.odd_sub 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd m ↔ Even n)
• Nat.odd_sub' 📋 Mathlib.Algebra.Ring.Parity
  {m n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd n ↔ Even m)
• Odd.mul 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} : Odd a → Odd b → Odd (a * b)
• Odd.neg 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} (hp : Odd a) : Odd (-a)
• odd_neg 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Odd (-a) ↔ Odd a
• Nat.odd_pow_iff 📋 Mathlib.Algebra.Ring.Parity
  {n e : ℕ} (he : e ≠ 0) : Odd (n ^ e) ↔ Odd n
• Even.add_odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} : Even a → Odd b → Odd (a + b)
• Even.odd_add 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} (ha : Even a) (hb : Odd b) : Odd (b + a)
• Odd.add_even 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} (ha : Odd a) (hb : Even b) : Odd (a + b)
• Odd.add_odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} : Odd a → Odd b → Even (a + b)
• odd_neg_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] : Odd (-1)
• Odd.map 📋 Mathlib.Algebra.Ring.Parity
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] {a : α} [FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a)
• Even.add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Even a) : Odd (a + 1)
• Even.one_add 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Even a) : Odd (1 + a)
• Odd.add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Odd a) : Even (a + 1)
• Odd.one_add 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Odd a) : Even (1 + a)
• Odd.of_isUnit_two 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] (h : IsUnit 2) (a : α) : Odd a
• Even.sub_odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a b : α} (ha : Even a) (hb : Odd b) : Odd (a - b)
• Nat.eight_dvd_sq_sub_one_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {k : ℕ} (hk : Odd k) : 8 ∣ k ^ 2 - 1
• Odd.sub_even 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Even b) : Odd (a - b)
• Odd.sub_odd 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Odd b) : Even (a - b)
• odd_add_one_self 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd (a + 1 + a)
• odd_add_one_self' 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd (a + (1 + a))
• odd_add_self_one' 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd (a + (a + 1))
• Nat.div_two_mul_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : n / 2 * 2 + 1 = n
• Nat.one_add_div_two_mul_two_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : 1 + n / 2 * 2 = n
• Nat.two_mul_div_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : 2 * (n / 2) + 1 = n
• even_add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Even (a + 1) ↔ Odd a
• odd_add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Odd (a + 1) ↔ Even a
• even_sub_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Even (a - 1) ↔ Odd a
• odd_sub_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Odd (a - 1) ↔ Even a
• Nat.mod_two_add_add_odd_mod_two 📋 Mathlib.Algebra.Ring.Parity
  (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1
• odd_add_two 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Odd (a + 2) ↔ Odd a
• odd_sub_two 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Ring α] {a : α} : Odd (a - 2) ↔ Odd a
• natCast_eq_one_of_odd_of_two_eq_zero 📋 Mathlib.Algebra.Ring.Parity
  {R : Type u_4} [AddMonoidWithOne R] {n : ℕ} (hn : Odd n) (h : 2 = 0) : ↑n = 1
• odd_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] (a : α) : Odd (2 * a + 1)
• Odd.neg_pow 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} : Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
• Odd.exists_bit1 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd a → ∃ b, a = 2 * b + 1
• odd_iff_exists_bit1 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd a ↔ ∃ b, a = 2 * b + 1
• range_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  (α : Type u_4) [Semiring α] : (Set.range fun x => 2 * x + 1) = {a | Odd a}
• Odd.neg_one_pow 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} (h : Odd n) : (-1) ^ n = -1
• Odd.pow_add_pow_eq_zero 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a b : α} {n : ℕ} [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) : a ^ n + b ^ n = 0
• neg_one_pow_eq_neg_one_iff_odd 📋 Mathlib.Algebra.Ring.Parity
  {R : Type u_4} [Monoid R] [HasDistribNeg R] {n : ℕ} (h : -1 ≠ 1) : (-1) ^ n = -1 ↔ Odd n
• Odd.intCast 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [Ring α] {n : ℤ} (hn : Odd n) : Odd ↑n
• Int.instDecidablePredOdd 📋 Mathlib.Algebra.Ring.Int.Parity
  : DecidablePred Odd
• Int.not_odd_zero 📋 Mathlib.Algebra.Ring.Int.Parity
  : ¬Odd 0
• Int.even_or_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  (n : ℤ) : Even n ∨ Odd n
• Int.even_xor'_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  (n : ℤ) : Xor (Even n) (Odd n)
• Int.even_xor_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  (n : ℤ) : Xor (Even n) (Odd n)
• Odd.natAbs 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → Odd n.natAbs
• Int.natAbs_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n.natAbs ↔ Odd n
• Int.not_even_iff_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : ¬Even n ↔ Odd n
• Int.not_odd_iff_even 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : ¬Odd n ↔ Even n
• Int.odd_coe_nat 📋 Mathlib.Algebra.Ring.Int.Parity
  (n : ℕ) : Odd ↑n ↔ Odd n
• Int.odd_sign_iff 📋 Mathlib.Algebra.Ring.Int.Parity
  {z : ℤ} : Odd z.sign ↔ z ≠ 0
• Int.ne_of_odd_add 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} (h : Odd (m + n)) : m ≠ n
• Int.Odd.of_mul_left 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} (h : Odd (m * n)) : Odd m
• Int.Odd.of_mul_right 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} (h : Odd (m * n)) : Odd n
• Int.even_add' 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Even (m + n) ↔ (Odd m ↔ Odd n)
• Int.even_sub' 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Even (m - n) ↔ (Odd m ↔ Odd n)
• Int.odd_add 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Odd (m + n) ↔ (Odd m ↔ Even n)
• Int.odd_add' 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Odd (m + n) ↔ (Odd n ↔ Even m)
• Int.odd_mul 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Odd (m * n) ↔ Odd m ∧ Odd n
• Int.odd_sub 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Odd (m - n) ↔ (Odd m ↔ Even n)
• Int.odd_sub' 📋 Mathlib.Algebra.Ring.Int.Parity
  {m n : ℤ} : Odd (m - n) ↔ (Odd n ↔ Even m)
• Int.odd_iff 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n ↔ n % 2 = 1
• Int.not_odd_iff 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : ¬Odd n ↔ n % 2 = 0
• Int.odd_pow' 📋 Mathlib.Algebra.Ring.Int.Parity
  {m : ℤ} {n : ℕ} (h : n ≠ 0) : Odd (m ^ n) ↔ Odd m
• Int.odd_pow 📋 Mathlib.Algebra.Ring.Int.Parity
  {m : ℤ} {n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0
• Int.sq_emod_four_eq_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {x : ℤ} (hx : Odd x) : x ^ 2 % 4 = 1
• Int.eight_dvd_sq_sub_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {k : ℤ} (hk : Odd k) : 8 ∣ k ^ 2 - 1
• Int.add_one_ediv_two_mul_two_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → 1 + n / 2 * 2 = n
• Int.ediv_two_mul_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → n / 2 * 2 + 1 = n
• Int.four_dvd_add_or_sub_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {a b : ℤ} (ha : Odd a) (hb : Odd b) : 4 ∣ a + b ∨ 4 ∣ a - b
• Int.two_mul_ediv_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → 2 * (n / 2) + 1 = n
• Int.two_mul_ediv_two_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} (h : Odd n) : 2 * (n / 2) = n - 1
• Odd.neg_zpow 📋 Mathlib.Algebra.Ring.Int.Parity
  {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) (a : α) : (-a) ^ n = -a ^ n
• Odd.neg_one_zpow 📋 Mathlib.Algebra.Ring.Int.Parity
  {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) : (-1) ^ n = -1
• Int.isCompl_even_odd 📋 Mathlib.Algebra.Order.Ring.Int
  : IsCompl {n | Even n} {n | Odd n}
• Nat.isCompl_even_odd 📋 Mathlib.Algebra.Order.Ring.Nat
  : IsCompl {n | Even n} {n | Odd n}
• Odd.pow_injective 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ} (hn : Odd n) : Function.Injective fun x => x ^ n
• Odd.pow_inj 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ} (hn : Odd n) {a b : R} : a ^ n = b ^ n ↔ a = b
• Odd.strictMono_pow 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : StrictMono fun a => a ^ n
• Odd.pow_le_pow 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ} (hn : Odd n) {a b : R} : a ^ n ≤ b ^ n ↔ a ≤ b
• Odd.pow_lt_pow 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ} (hn : Odd n) {a b : R} : a ^ n < b ^ n ↔ a < b
• Odd.pow_neg 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : a < 0 → a ^ n < 0
• Odd.pow_nonpos 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : a ≤ 0 → a ^ n ≤ 0
• Odd.pow_neg_iff 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : a ^ n < 0 ↔ a < 0
• Odd.pow_nonneg_iff 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a
• Odd.pow_nonpos_iff 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0
• Odd.pow_pos_iff 📋 Mathlib.Algebra.Order.Ring.Basic
  {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) : 0 < a ^ n ↔ 0 < a
• Odd.of_dvd_nat 📋 Mathlib.Algebra.Order.Ring.Abs
  {m n : ℕ} (hn : Odd n) (hm : m ∣ n) : Odd m
• Odd.ne_two_of_dvd_nat 📋 Mathlib.Algebra.Order.Ring.Abs
  {m n : ℕ} (hn : Odd n) (hm : m ∣ n) : m ≠ 2
• Odd.mod_even 📋 Mathlib.Algebra.Order.Ring.Abs
  {n a : ℕ} (hn : Odd n) (ha : Even a) : Odd (n % a)
• Odd.mod_even_iff 📋 Mathlib.Algebra.Order.Ring.Abs
  {n a : ℕ} (ha : Even a) : Odd (n % a) ↔ Odd n
• odd_abs 📋 Mathlib.Algebra.Order.Ring.Abs
  {α : Type u_1} [LinearOrder α] [Ring α] {a : α} : Odd |a| ↔ Odd a
• pow_eq_neg_one_iff 📋 Mathlib.Algebra.Order.Ring.Abs
  {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} : a ^ n = -1 ↔ a = -1 ∧ Odd n
• pow_eq_neg_pow_iff 📋 Mathlib.Algebra.Order.Ring.Abs
  {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n
• Odd.pos 📋 Mathlib.Algebra.Order.Ring.Canonical
  {R : Type u} [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R} : Odd a → 0 < a
• Set.odd_ncard_compl_iff 📋 Mathlib.Data.Set.Card
  {α : Type u_1} [Finite α] (heven : Even (Nat.card α)) (s : Set α) : Odd sᶜ.ncard ↔ Odd s.ncard
• Set.even_card_insert_iff 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) : Even (insert a s).ncard ↔ Odd s.ncard
• Set.odd_card_insert_iff 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) : Odd (insert a s).ncard ↔ Even s.ncard
• Odd.isCoprime_two 📋 Mathlib.RingTheory.Coprime.Basic
  {R : Type u} [CommRing R] {x : R} (h : Odd x) : IsCoprime x 2
• Odd.nat_add_dvd_pow_add_pow 📋 Mathlib.Algebra.Ring.GeomSum
  (x y : ℕ) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n
• Odd.add_dvd_pow_add_pow 📋 Mathlib.Algebra.Ring.GeomSum
  {R : Type u_1} [CommRing R] (x y : R) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n
• Odd.coprime_two_left 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : Odd n → Nat.Coprime 2 n
• Odd.coprime_two_right 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : Odd n → n.Coprime 2
• Nat.Coprime.odd_of_left 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : Nat.Coprime 2 n → Odd n
• Nat.Coprime.odd_of_right 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n.Coprime 2 → Odd n
• Nat.coprime_two_left 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : Nat.Coprime 2 n ↔ Odd n
• Nat.coprime_two_right 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n.Coprime 2 ↔ Odd n
• Nat.Prime.odd_of_ne_two 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) : Odd p
• Nat.Prime.eq_two_or_odd' 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : p = 2 ∨ Odd p
• Nat.Prime.odd_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : Odd p ↔ 3 ≤ p
• Nat.forall_prime_of_two_of_odd 📋 Mathlib.Data.Nat.Prime.Basic
  {P : ℕ → Prop} : (P 2 ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → P p) → ∀ (p : ℕ), Nat.Prime p → P p
• Nat.forall_prime_iff_two_and_odd 📋 Mathlib.Data.Nat.Prime.Basic
  {P : ℕ → Prop} : (∀ (p : ℕ), Nat.Prime p → P p) ↔ P 2 ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → P p
• Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt 📋 Mathlib.Data.Nat.Factors
  {n : ℕ} (n2 : 2 < n) : 4 ∣ n ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
• Nat.eq_two_pow_or_exists_odd_prime_and_dvd 📋 Mathlib.Data.Nat.Factors
  (n : ℕ) : (∃ k, n = 2 ^ k) ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
• exists_nsmul_eq_nsmul_two_add 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} (hx : p • x = 0) (hp : Odd p) (n : ℕ) : ∃ m, n • x = (2 * m) • x
• exists_pow_eq_pow_two_mul 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} (hx : x ^ p = 1) (hp : Odd p) (n : ℕ) : ∃ m, x ^ n = x ^ (2 * m)
• ZMod.ne_neg_self 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) : a ≠ -a
• ZMod.add_self_eq_zero_iff_eq_zero 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} (hn : Odd n) {a : ZMod n} : a + a = 0 ↔ a = 0
• Odd.intCast_zmod_two 📋 Mathlib.Data.ZMod.Basic
  {n : ℤ} : Odd n → ↑n = 1
• ZMod.intCast_eq_one_iff_odd 📋 Mathlib.Data.ZMod.Basic
  {n : ℤ} : ↑n = 1 ↔ Odd n
• Odd.natCast_zmod_two 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} : Odd n → ↑n = 1
• ZMod.natCast_eq_one_iff_odd 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} : ↑n = 1 ↔ Odd n
• ZMod.natCast_ne_zero_iff_odd 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} : ↑n ≠ 0 ↔ Odd n
• Odd.geom_sum_pos 📋 Mathlib.Algebra.Order.Ring.GeomSum
  {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (h : Odd n) : 0 < ∑ i ∈ Finset.range n, x ^ i
• geom_sum_pos_iff 📋 Mathlib.Algebra.Order.Ring.GeomSum
  {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1
• Nat.exists_eq_two_pow_mul_odd 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (hn : n ≠ 0) : ∃ k m, Odd m ∧ n = 2 ^ k * m
• Finset.even_sum_iff_even_card_odd 📋 Mathlib.Algebra.BigOperators.Ring.Nat
  {ι : Type u_1} {s : Finset ι} (f : ι → ℕ) : Even (∑ i ∈ s, f i) ↔ Even {x ∈ s | Odd (f x)}.card
• Finset.odd_sum_iff_odd_card_odd 📋 Mathlib.Algebra.BigOperators.Ring.Nat
  {ι : Type u_1} {s : Finset ι} (f : ι → ℕ) : Odd (∑ i ∈ s, f i) ↔ Odd {x ∈ s | Odd (f x)}.card
• Equiv.Perm.sign_of_cycleType_eq_replicate 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : ℕ} (hn : 0 < n) (hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n) : Equiv.Perm.sign σ = if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
• Int.negOnePow_odd 📋 Mathlib.Algebra.Ring.NegOnePow
  (n : ℤ) (hn : Odd n) : n.negOnePow = -1
• Int.negOnePow_eq_neg_one_iff 📋 Mathlib.Algebra.Ring.NegOnePow
  (n : ℤ) : n.negOnePow = -1 ↔ Odd n
• Nat.odd_totient_iff_eq_one 📋 Mathlib.Data.Nat.Totient
  {n : ℕ} : Odd n.totient ↔ n.totient = 1
• Nat.totient_two_mul_of_odd 📋 Mathlib.Data.Nat.Totient
  {n : ℕ} (hn : Odd n) : (2 * n).totient = n.totient
• Nat.odd_totient_iff 📋 Mathlib.Data.Nat.Totient
  {n : ℕ} : Odd n.totient ↔ n = 1 ∨ n = 2
• Odd.all 📋 Mathlib.Algebra.CharP.Invertible
  {R : Type u_1} [Ring R] [Invertible 2] (a : R) : Odd a
• ComplexShape.down_nat_odd_add 📋 Mathlib.Algebra.Homology.AlternatingConst
  {i j : ℕ} (h : (ComplexShape.down ℕ).Rel i j) : Odd (i + j)
• ComplexShape.up_nat_odd_add 📋 Mathlib.Algebra.Homology.AlternatingConst
  {i j : ℕ} (h : (ComplexShape.up ℕ).Rel i j) : Odd (i + j)
• ChainComplex.alternatingConstHomologyDataOdd 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ) (hn : Odd n) : (HomologicalComplex.sc (ChainComplex.alternatingConst.obj X) n).HomologyData
• HomologicalComplex.alternatingConst 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) : HomologicalComplex C c
• HomologicalComplex.alternatingConst_X 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (n : ℕ) : (HomologicalComplex.alternatingConst A hOdd hEven hc).X n = A
• HomologicalComplex.alternatingConstScIsoEven 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Even j) : (HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k ≅ { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }
• HomologicalComplex.alternatingConstScIsoOdd 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Odd j) : (HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k ≅ { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }
• HomologicalComplex.alternatingConst_d 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (i j : ℕ) : (HomologicalComplex.alternatingConst A hOdd hEven hc).d i j = if c.Rel i j then if Even i then φ else ψ else 0
• HomologicalComplex.alternatingConstHomologyIsoEven 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) : (HomologicalComplex.alternatingConst A hOdd hEven hc).homology j ≅ { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.homology
• HomologicalComplex.alternatingConstHomologyIsoOdd 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) : (HomologicalComplex.alternatingConst A hOdd hEven hc).homology j ≅ { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.homology
• HomologicalComplex.alternatingConst_iCycles_even_comp 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) φ = 0
• HomologicalComplex.alternatingConst_iCycles_odd_comp 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) ψ = 0
• HomologicalComplex.alternatingConst_iCycles_even_comp_assoc 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) (CategoryTheory.CategoryStruct.comp φ h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• HomologicalComplex.alternatingConst_iCycles_odd_comp_assoc 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) (CategoryTheory.CategoryStruct.comp ψ h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• HomologicalComplex.alternatingConst_iCycles_even_comp_apply 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((HomologicalComplex.alternatingConst A hOdd hEven hc).cycles j)) : (CategoryTheory.ConcreteCategory.hom φ) ((CategoryTheory.ConcreteCategory.hom ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j)) x) = (CategoryTheory.ConcreteCategory.hom 0) x
• HomologicalComplex.alternatingConst_iCycles_odd_comp_apply 📋 Mathlib.Algebra.Homology.AlternatingConst
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((HomologicalComplex.alternatingConst A hOdd hEven hc).cycles j)) : (CategoryTheory.ConcreteCategory.hom ψ) ((CategoryTheory.ConcreteCategory.hom ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j)) x) = (CategoryTheory.ConcreteCategory.hom 0) x
• Polynomial.Chebyshev.T_eval_zero_of_odd 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] {n : ℤ} (hn : Odd n) : Polynomial.eval 0 (Polynomial.Chebyshev.T R n) = 0
• Polynomial.Chebyshev.U_eval_zero_of_odd 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] {n : ℤ} (hn : Odd n) : Polynomial.eval 0 (Polynomial.Chebyshev.U R n) = 0
• Fin.even_of_odd 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} (hn : Odd n) (k : Fin n) : Even k
• Fin.even_iff 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} : Even k ↔ Odd n ∨ Even ↑k
• Fin.odd_of_odd 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} [NeZero n] (hn : Odd n) (k : Fin n) : Odd k
• Fin.odd_of_val 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] (h : Odd ↑k) : Odd k
• Fin.odd_iff_imp 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] : Odd k ↔ Even n → Odd ↑k
• Fin.odd_iff_of_even 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] (hn : Even n) : Odd k ↔ Odd ↑k
• Fin.not_even_iff_odd_of_even 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] (hn : Even n) : ¬Even k ↔ Odd k
• Fin.not_odd_iff_even_of_even 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] (hn : Even n) : ¬Odd k ↔ Even k
• Fin.odd_iff 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] : Odd k ↔ Odd n ∨ Odd ↑k
• Fin.even_add_one_iff_odd 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] : Even (k + 1) ↔ Odd k
• Fin.odd_add_one_iff_even 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] : Odd (k + 1) ↔ Even k
• Fin.odd_iff_mod_of_even 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} {k : Fin n} [NeZero n] (hn : Even n) : Odd k ↔ ↑k % 2 = 1
• Fin.even_succAbove_add_predAbove 📋 Mathlib.Data.Fin.Parity
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
• SignType.zpow_odd 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {z : ℤ} (hz : Odd z) : s ^ z = s
• SignType.pow_odd 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {n : ℕ} (hn : Odd n) : s ^ n = s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c