Loogle!

Result

Found 211 declarations mentioning Nat.ModEq. Of these, only the first 200 are shown.

• Nat.ModEq 📋 Mathlib.Data.Nat.ModEq
  (n a b : ℕ) : Prop
• Nat.ModEq.instRefl 📋 Mathlib.Data.Nat.ModEq
  {n : ℕ} : Std.Refl n.ModEq
• Nat.ModEq.refl 📋 Mathlib.Data.Nat.ModEq
  {n : ℕ} (a : ℕ) : a ≡ a [MOD n]
• Nat.ModEq.rfl 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} : a ≡ a [MOD n]
• Nat.instDecidableModEq 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : Decidable (a ≡ b [MOD n])
• Nat.modulus_modEq_zero 📋 Mathlib.Data.Nat.ModEq
  {n : ℕ} : n ≡ 0 [MOD n]
• Nat.modEq_one 📋 Mathlib.Data.Nat.ModEq
  {a b : ℕ} : a ≡ b [MOD 1]
• Nat.ModEq.instTrans 📋 Mathlib.Data.Nat.ModEq
  {n : ℕ} : Trans n.ModEq n.ModEq n.ModEq
• Nat.ModEq.symm 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ b [MOD n] → b ≡ a [MOD n]
• Nat.ModEq.comm 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ b [MOD n] ↔ b ≡ a [MOD n]
• AddCommGroup.modEq_iff_natModEq 📋 Mathlib.Data.Nat.ModEq
  {a b n : ℕ} : a ≡ b [PMOD n] ↔ a ≡ b [MOD n]
• Nat.add_modEq_left 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} : n + a ≡ a [MOD n]
• Nat.add_modEq_right 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} : a + n ≡ a [MOD n]
• Nat.mod_modEq 📋 Mathlib.Data.Nat.ModEq
  (a n : ℕ) : a % n ≡ a [MOD n]
• Nat.modEq_zero_iff 📋 Mathlib.Data.Nat.ModEq
  {a b : ℕ} : a ≡ b [MOD 0] ↔ a = b
• Dvd.dvd.modEq_zero_nat 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} (h : n ∣ a) : a ≡ 0 [MOD n]
• Dvd.dvd.zero_modEq_nat 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} (h : n ∣ a) : 0 ≡ a [MOD n]
• Nat.ModEq.gcd_eq 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} (h : a ≡ b [MOD m]) : a.gcd m = b.gcd m
• Nat.modEq_zero_iff_dvd 📋 Mathlib.Data.Nat.ModEq
  {n a : ℕ} : a ≡ 0 [MOD n] ↔ n ∣ a
• Nat.ModEq.trans 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n]
• Nat.ModEq.of_dvd 📋 Mathlib.Data.Nat.ModEq
  {m n a b : ℕ} (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m]
• Nat.mod_lcm 📋 Mathlib.Data.Nat.ModEq
  {m n a b : ℕ} (hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) : a ≡ b [MOD n.lcm m]
• Nat.chineseRemainder 📋 Mathlib.Data.Nat.ModEq
  {m n : ℕ} (co : n.Coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }
• Nat.modEq_sub 📋 Mathlib.Data.Nat.ModEq
  {a b : ℕ} (h : b ≤ a) : a ≡ b [MOD a - b]
• Nat.add_modulus_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
• Nat.modEq_add_modulus_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ b + n [MOD n] ↔ a ≡ b [MOD n]
• Nat.modEq_modulus_add_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ n + b [MOD n] ↔ a ≡ b [MOD n]
• Nat.modulus_add_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]
• Nat.ModEq.dvd' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : a ≡ b [MOD n]) : n ∣ b - a
• Nat.ModEq.of_mul_left 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n]
• Nat.ModEq.of_mul_right 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n]
• Nat.add_modEq_left_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a + b ≡ a [MOD n] ↔ n ∣ b
• Nat.add_modEq_right_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a + b ≡ b [MOD n] ↔ n ∣ a
• Nat.left_modEq_add_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ a + b [MOD n] ↔ n ∣ b
• Nat.right_modEq_add_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : b ≡ a + b [MOD n] ↔ n ∣ a
• Nat.ModEq.eq_of_lt_of_lt 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) : a = b
• Nat.chineseRemainder' 📋 Mathlib.Data.Nat.ModEq
  {m n a b : ℕ} (h : a ≡ b [MOD n.gcd m]) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }
• Nat.coprime_of_mul_modEq_one 📋 Mathlib.Data.Nat.ModEq
  (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n
• Nat.ModEq.modulus_mul_add 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} : m * a + b ≡ b [MOD m]
• Nat.mod_eq_of_modEq 📋 Mathlib.Data.Nat.ModEq
  {a b n : ℕ} (h : a ≡ b [MOD n]) (hb : b < n) : a % n = b
• Nat.ModEq.dvd_iff 📋 Mathlib.Data.Nat.ModEq
  {m a b d : ℕ} (h : a ≡ b [MOD m]) (hdm : d ∣ m) : d ∣ a ↔ d ∣ b
• Nat.modEq_of_dvd' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : a ≤ b) : n ∣ b - a → a ≡ b [MOD n]
• Nat.modEq_sub_modulus_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : n ≤ b) : a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]
• Nat.sub_modulus_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : n ≤ a) : a - n ≡ b [MOD n] ↔ a ≡ b [MOD n]
• Nat.ModEq.add_le_of_lt 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} (h1 : a ≡ b [MOD m]) (h2 : a < b) : a + m ≤ b
• Nat.ModEq.le_of_lt_add 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} (h1 : a ≡ b [MOD m]) (h2 : a < b + m) : a ≤ b
• Nat.modEq_iff_dvd' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a
• Nat.ModEq.add_left 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : c + a ≡ c + b [MOD n]
• Nat.ModEq.add_left_cancel' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : c + a ≡ c + b [MOD n]) : a ≡ b [MOD n]
• Nat.ModEq.add_right 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : a + c ≡ b + c [MOD n]
• Nat.ModEq.add_right_cancel' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a + c ≡ b + c [MOD n]) : a ≡ b [MOD n]
• Nat.ModEq.mul_left 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD n]
• Nat.ModEq.mul_right 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n]
• Nat.add_modulus_mul_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
• Nat.add_mul_modulus_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
• Nat.modEq_add_modulus_mul_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a ≡ b + n * c [MOD n] ↔ a ≡ b [MOD n]
• Nat.modEq_add_mul_modulus_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a ≡ b + c * n [MOD n] ↔ a ≡ b [MOD n]
• Nat.modEq_and_modEq_iff_modEq_mul 📋 Mathlib.Data.Nat.ModEq
  {a b m n : ℕ} (hmn : m.Coprime n) : a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n]
• Nat.modEq_modulus_mul_add_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]
• Nat.modEq_mul_modulus_add_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]
• Nat.modEq_of_dvd 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : ↑n ∣ ↑b - ↑a → a ≡ b [MOD n]
• Nat.modulus_mul_add_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
• Nat.mul_modulus_add_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} : b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
• Nat.ModEq.dvd 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ b [MOD n] → ↑n ∣ ↑b - ↑a
• Nat.modEq_iff_dvd 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} : a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
• Nat.ext_div_modEq 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h0 : a / n = b / n) (h1 : a ≡ b [MOD n]) : a = b
• Nat.modEq_iff_eq_of_div_eq 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : a / n = b / n) : a ≡ b [MOD n] ↔ a = b
• Nat.ext_div_modEq_iff 📋 Mathlib.Data.Nat.ModEq
  (n a b : ℕ) : a = b ↔ a / n = b / n ∧ a ≡ b [MOD n]
• Nat.ModEq.add 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n]
• Nat.ModEq.add_left_cancel 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : c ≡ d [MOD n]
• Nat.ModEq.add_right_cancel 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : a ≡ b [MOD n]
• Nat.ModEq.mul 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a * c ≡ b * d [MOD n]
• Nat.ModEq.add_iff_left 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h : a ≡ b [MOD n]) : a + c ≡ b + d [MOD n] ↔ c ≡ d [MOD n]
• Nat.ModEq.add_iff_right 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] ↔ a ≡ b [MOD n]
• Nat.modEq_iff_exists_eq_add 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (h : a ≤ b) : a ≡ b [MOD n] ↔ ∃ t, b = a + n * t
• Nat.ModEq.mul_left' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD c * n]
• Nat.ModEq.mul_right' 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n * c]
• Nat.ModEq.eq_of_abs_lt 📋 Mathlib.Data.Nat.ModEq
  {m a b : ℕ} (h : a ≡ b [MOD m]) (h2 : |↑b - ↑a| < ↑m) : a = b
• Nat.ModEq.cancel_left_of_coprime 📋 Mathlib.Data.Nat.ModEq
  {m a b c : ℕ} (hmc : m.gcd c = 1) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m]
• Nat.ModEq.cancel_right_of_coprime 📋 Mathlib.Data.Nat.ModEq
  {m a b c : ℕ} (hmc : m.gcd c = 1) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m]
• Nat.ModEq.pow 📋 Mathlib.Data.Nat.ModEq
  {n a b : ℕ} (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n]
• Nat.ModEq.sub_left 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} (hba : b ≤ a) (hca : c ≤ a) (hbc : b ≡ c [MOD n]) : a - b ≡ a - c [MOD n]
• Nat.ModEq.sub_right 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} (hab : a ≤ b) (hac : a ≤ c) (hbc : b ≡ c [MOD n]) : b - a ≡ c - a [MOD n]
• AddCommGroup.ModEq.natCast 📋 Mathlib.Data.Nat.ModEq
  {M : Type u_1} [AddCommMonoidWithOne M] {a b n : ℕ} (h : a ≡ b [MOD n]) : ↑a ≡ ↑b [PMOD ↑n]
• Nat.ModEq.sub_left' 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} (h : b ≤ a ↔ c ≤ a) (hbc : b ≡ c [MOD n]) : a - b ≡ a - c [MOD n]
• Nat.ModEq.sub_right' 📋 Mathlib.Data.Nat.ModEq
  {n a b c : ℕ} (h : a ≤ b ↔ a ≤ c) (hbc : b ≡ c [MOD n]) : b - a ≡ c - a [MOD n]
• Nat.ModEq.sub 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (hca : c ≤ a) (hdb : d ≤ b) (hab : a ≡ b [MOD n]) (hcd : c ≡ d [MOD n]) : a - c ≡ b - d [MOD n]
• Nat.ModEq.mul_left_cancel' 📋 Mathlib.Data.Nat.ModEq
  {a b c m : ℕ} (hc : c ≠ 0) : c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
• Nat.ModEq.mul_right_cancel' 📋 Mathlib.Data.Nat.ModEq
  {a b c m : ℕ} (hc : c ≠ 0) : a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
• Nat.ModEq.of_natCast 📋 Mathlib.Data.Nat.ModEq
  {M : Type u_1} [AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] → a ≡ b [MOD n]
• Nat.ModEq.sub' 📋 Mathlib.Data.Nat.ModEq
  {n a b c d : ℕ} (h : c ≤ a ↔ d ≤ b) (hab : a ≡ b [MOD n]) (hcd : c ≡ d [MOD n]) : a - c ≡ b - d [MOD n]
• AddCommGroup.natCast_modEq_natCast 📋 Mathlib.Data.Nat.ModEq
  {M : Type u_1} [AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
• Nat.chineseRemainder_modEq_unique 📋 Mathlib.Data.Nat.ModEq
  {m n : ℕ} (co : n.Coprime m) {a b z : ℕ} (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) : z ≡ ↑(Nat.chineseRemainder co a b) [MOD n * m]
• Nat.ModEq.mul_left_cancel_iff' 📋 Mathlib.Data.Nat.ModEq
  {a b c m : ℕ} (hc : c ≠ 0) : c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m]
• Nat.ModEq.mul_right_cancel_iff' 📋 Mathlib.Data.Nat.ModEq
  {a b c m : ℕ} (hc : c ≠ 0) : a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m]
• Nat.ModEq.cancel_left_div_gcd 📋 Mathlib.Data.Nat.ModEq
  {m a b c : ℕ} (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m / m.gcd c]
• Nat.ModEq.cancel_right_div_gcd 📋 Mathlib.Data.Nat.ModEq
  {m a b c : ℕ} (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m / m.gcd c]
• Nat.chineseRemainder'_lt_lcm 📋 Mathlib.Data.Nat.ModEq
  {m n a b : ℕ} (h : a ≡ b [MOD n.gcd m]) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(Nat.chineseRemainder' h) < n.lcm m
• Nat.ModEq.of_div 📋 Mathlib.Data.Nat.ModEq
  {m a b c : ℕ} (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) : c ∣ b → c ∣ m → a ≡ b [MOD m]
• Nat.ModEq.cancel_left_div_gcd' 📋 Mathlib.Data.Nat.ModEq
  {m a b c d : ℕ} (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : c * a ≡ d * b [MOD m]) : a ≡ b [MOD m / m.gcd c]
• Nat.ModEq.cancel_right_div_gcd' 📋 Mathlib.Data.Nat.ModEq
  {m a b c d : ℕ} (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : a * c ≡ b * d [MOD m]) : a ≡ b [MOD m / m.gcd c]
• Nat.chineseRemainder_lt_mul 📋 Mathlib.Data.Nat.ModEq
  {m n : ℕ} (co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(Nat.chineseRemainder co a b) < n * m
• Int.natCast_modEq_iff 📋 Mathlib.Data.Int.ModEq
  {a b n : ℕ} : ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
• CharP.natCast_eq_natCast' 📋 Mathlib.Algebra.CharP.Basic
  (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) : ↑a = ↑b
• CharP.natCast_eq_natCast 📋 Mathlib.Algebra.CharP.Basic
  (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R] : ↑a = ↑b ↔ a ≡ b [MOD p]
• nsmul_eq_zero_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} : n • x = 0 ↔ n ≡ 0 [MOD addOrderOf x]
• pow_eq_one_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {n : ℕ} : x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
• IsOfFinAddOrder.nsmul_eq_nsmul_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {n m : ℕ} (hx : IsOfFinAddOrder x) : n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
• IsOfFinOrder.pow_eq_pow_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {n m : ℕ} (hx : IsOfFinOrder x) : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
• nsmul_eq_nsmul_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {m n : ℕ} : n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
• pow_eq_pow_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [LeftCancelMonoid G] {x : G} {m n : ℕ} : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
• AddRightCancelMonoid.nsmul_eq_nsmul_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddRightCancelMonoid G] {x : G} {m n : ℕ} : n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
• RightCancelMonoid.pow_eq_pow_iff_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [RightCancelMonoid G] {x : G} {m n : ℕ} : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
• nsmul_eq_nsmul_of_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {n a b : ℕ} (h : a ≡ b [MOD n]) (hx : n • x = 0) : a • x = b • x
• pow_eq_pow_of_modEq 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {n a b : ℕ} (h : a ≡ b [MOD n]) (hx : x ^ n = 1) : x ^ a = x ^ b
• ZMod.natCast_eq_natCast_iff 📋 Mathlib.Data.ZMod.Basic
  (a b c : ℕ) : ↑a = ↑b ↔ a ≡ b [MOD c]
• Nat.ofDigits_modEq' 📋 Mathlib.Data.Nat.Digits.Lemmas
  (b b' k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits b' L [MOD k]
• Nat.ofDigits_modEq 📋 Mathlib.Data.Nat.Digits.Lemmas
  (b k : ℕ) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits (b % k) L [MOD k]
• Nat.modEq_digits_sum 📋 Mathlib.Data.Nat.Digits.Lemmas
  (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (b'.digits n).sum [MOD b]
• Nat.ModEq.multisetProd_one 📋 Mathlib.Algebra.BigOperators.ModEq
  {n : ℕ} {s : Multiset ℕ} (h : ∀ x ∈ s, x ≡ 1 [MOD n]) : s.prod ≡ 1 [MOD n]
• Nat.ModEq.multisetSum_zero 📋 Mathlib.Algebra.BigOperators.ModEq
  {n : ℕ} {s : Multiset ℕ} (h : ∀ x ∈ s, x ≡ 0 [MOD n]) : s.sum ≡ 0 [MOD n]
• Nat.ModEq.listProd_one 📋 Mathlib.Algebra.BigOperators.ModEq
  {n : ℕ} {l : List ℕ} (h : ∀ x ∈ l, x ≡ 1 [MOD n]) : l.prod ≡ 1 [MOD n]
• Nat.ModEq.listSum_zero 📋 Mathlib.Algebra.BigOperators.ModEq
  {n : ℕ} {l : List ℕ} (h : ∀ x ∈ l, x ≡ 0 [MOD n]) : l.sum ≡ 0 [MOD n]
• Nat.ModEq.multisetProd_map_one 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 1 [MOD n]) : (Multiset.map f s).prod ≡ 1 [MOD n]
• Nat.ModEq.multisetSum_map_zero 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 0 [MOD n]) : (Multiset.map f s).sum ≡ 0 [MOD n]
• Nat.ModEq.listProd_map_one 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ} (h : ∀ x ∈ l, f x ≡ 1 [MOD n]) : (List.map f l).prod ≡ 1 [MOD n]
• Nat.ModEq.multisetProd_map 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]
• Nat.ModEq.multisetSum_map 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]
• Nat.ModEq.listSum_map_zero 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ} (h : ∀ x ∈ l, f x ≡ 0 [MOD n]) : (List.map f l).sum ≡ 0 [MOD n]
• Nat.ModEq.listProd_map 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ} (h : ∀ x ∈ l, f x ≡ g x [MOD n]) : (List.map f l).prod ≡ (List.map g l).prod [MOD n]
• Nat.ModEq.prod_one 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ 1 [MOD n]
• Nat.ModEq.sum_zero 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ 0 [MOD n]
• Nat.ModEq.prod 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n]
• Nat.ModEq.sum 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [MOD n]
• Nat.ModEq.listSum_map 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ} (h : ∀ x ∈ l, f x ≡ g x [MOD n]) : (List.map f l).sum ≡ (List.map g l).sum [MOD n]
• Nat.prod_modEq_single 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 1 [MOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ f a [MOD n]
• Nat.sum_modEq_single 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 0 [MOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ f a [MOD n]
• Nat.prod_modEq_ite 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]
• Nat.sum_modEq_ite 📋 Mathlib.Algebra.BigOperators.ModEq
  {α : Type u_1} {n : ℕ} {f : α → ℕ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]
• Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
  {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card]
• Equiv.Perm.card_compl_support_modEq 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {p n : ℕ} [hp : Fact (Nat.Prime p)] {σ : Equiv.Perm α} (hσ : σ ^ p ^ n = 1) : σ.supportᶜ.card ≡ Fintype.card α [MOD p]
• Equiv.Perm.card_fixedPoints_modEq 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {f : Function.End α} {p n : ℕ} [hp : Fact (Nat.Prime p)] (hf : f ^ p ^ n = 1) : Fintype.card α ≡ Fintype.card ↑(Function.fixedPoints f) [MOD p]
• IsPGroup.card_modEq_card_fixedPoints 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (α : Type u_2) [MulAction G α] [Finite α] : Nat.card α ≡ Nat.card ↑(MulAction.fixedPoints G α) [MOD p]
• card_sylow_modEq_one 📋 Mathlib.GroupTheory.Sylow
  (p : ℕ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] : Nat.card (Sylow p G) ≡ 1 [MOD p]
• Sylow.card_normalizer_modEq_card 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Nat.card ↥H = p ^ n) : Nat.card ↥(Subgroup.normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]
• Sylow.card_quotient_normalizer_modEq_card_quotient 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Nat.card ↥H = p ^ n) : Nat.card (↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H) ≡ Nat.card (G ⧸ H) [MOD p]
• Nat.frequently_modEq 📋 Mathlib.Order.Filter.AtTopBot.ModEq
  {n : ℕ} (h : n ≠ 0) (d : ℕ) : ∃ᶠ (m : ℕ) in Filter.atTop, m ≡ d [MOD n]
• Nat.ModEq.pow_totient 📋 Mathlib.FieldTheory.Finite.Basic
  {x n : ℕ} (h : x.Coprime n) : x ^ n.totient ≡ 1 [MOD n]
• Nat.ModEq.pow_card_sub_one_eq_one 📋 Mathlib.FieldTheory.Finite.Basic
  {p : ℕ} (hp : Nat.Prime p) {n : ℕ} (hpn : n.Coprime p) : n ^ (p - 1) ≡ 1 [MOD p]
• pow_pow_modEq_one 📋 Mathlib.FieldTheory.Finite.Basic
  (p m a : ℕ) : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
• Nat.sq_add_sq_modEq 📋 Mathlib.FieldTheory.Finite.Basic
  (p : ℕ) [Fact (Nat.Prime p)] (x : ℕ) : ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]
• IsPrimitiveRoot.primitiveRootsPowEquiv 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] [IsDomain R] {a b n : ℕ} (h : a * b ≡ 1 [MOD n]) : ↥(primitiveRoots n R) ≃ ↥(primitiveRoots n R)
• IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] [IsDomain R] {a b n : ℕ} (h : a * b ≡ 1 [MOD n]) (x : ↥(primitiveRoots n R)) : ↑((IsPrimitiveRoot.primitiveRootsPowEquiv h) x) = ↑x ^ a
• IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] [IsDomain R] {a b n : ℕ} (h : a * b ≡ 1 [MOD n]) (x : ↥(primitiveRoots n R)) : ↑((IsPrimitiveRoot.primitiveRootsPowEquiv h).symm x) = ↑x ^ b
• Nat.exists_lt_modEq_of_infinite 📋 Mathlib.Combinatorics.Pigeonhole
  {s : Set ℕ} (hs : s.Infinite) {k : ℕ} (hk : 0 < k) : ∃ m ∈ s, ∃ n ∈ s, m < n ∧ m ≡ n [MOD k]
• schnirelmannDensity_setOfPred_modeq_one 📋 Mathlib.Combinatorics.Schnirelmann
  {m : ℕ} : schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
• schnirelmannDensity_setOf_modeq_one 📋 Mathlib.Combinatorics.Schnirelmann
  {m : ℕ} : schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
• Nat.count_modEq_card_eq_ceil 📋 Mathlib.Data.Int.CardIntervalMod
  (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑(Nat.count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉
• Nat.Ico_filter_modEq_cast 📋 Mathlib.Data.Int.CardIntervalMod
  (a b : ℕ) {r v : ℕ} : Finset.map Nat.castEmbedding ({x ∈ Finset.Ico a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
• Nat.Ioc_filter_modEq_cast 📋 Mathlib.Data.Int.CardIntervalMod
  (a b : ℕ) {r v : ℕ} : Finset.map Nat.castEmbedding ({x ∈ Finset.Ioc a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
• Nat.count_modEq_card 📋 Mathlib.Data.Int.CardIntervalMod
  (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : Nat.count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
• Nat.Ico_filter_modEq_card 📋 Mathlib.Data.Int.CardIntervalMod
  (a b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑{x ∈ Finset.Ico a b | x ≡ v [MOD r]}.card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
• Nat.Ioc_filter_modEq_card 📋 Mathlib.Data.Int.CardIntervalMod
  (a b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑{x ∈ Finset.Ioc a b | x ≡ v [MOD r]}.card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
• Nat.modEq_list_prod_iff 📋 Mathlib.Data.Nat.ChineseRemainder
  {a b : ℕ} {l : List ℕ} (co : List.Pairwise Nat.Coprime l) : a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
• Nat.chineseRemainderOfList 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) (l : List ι) : List.Pairwise (Function.onFun Nat.Coprime s) l → { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
• Nat.modEq_list_map_prod_iff 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} {a b : ℕ} {s : ι → ℕ} {l : List ι} (co : List.Pairwise (Function.onFun Nat.Coprime s) l) : a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
• Nat.chineseRemainderOfList_nil 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) : ↑(Nat.chineseRemainderOfList a s [] ⋯) = 0
• Nat.chineseRemainderOfMultiset 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} : m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] }
• Nat.chineseRemainderOfFinset 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0) (pp : (↑t).Pairwise (Function.onFun Nat.Coprime s)) : { k // ∀ i ∈ t, k ≡ a i [MOD s i] }
• Nat.chineseRemainderOfList_modEq_unique 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) l) {z : ℕ} (hz : ∀ i ∈ l, z ≡ a i [MOD s i]) : z ≡ ↑(Nat.chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
• Nat.chineseRemainderOfList_lt_prod 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) l) (hs : ∀ i ∈ l, s i ≠ 0) : ↑(Nat.chineseRemainderOfList a s l co) < (List.map s l).prod
• Nat.chineseRemainderOfFinset_lt_prod 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) {t : Finset ι} (hs : ∀ i ∈ t, s i ≠ 0) (pp : (↑t).Pairwise (Function.onFun Nat.Coprime s)) : ↑(Nat.chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i
• Nat.chineseRemainderOfMultiset_lt_prod 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0) (pp : {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s)) : ↑(Nat.chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod
• Nat.chineseRemainderOfList_perm 📋 Mathlib.Data.Nat.ChineseRemainder
  {ι : Type u_1} (a s : ι → ℕ) {l l' : List ι} (hl : l.Perm l') (hs : ∀ i ∈ l, s i ≠ 0) (co : List.Pairwise (Function.onFun Nat.Coprime s) l) : ↑(Nat.chineseRemainderOfList a s l co) = ↑(Nat.chineseRemainderOfList a s l' ⋯)
• Choose.choose_mul_mul_modEq_choose_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {a b p : ℕ} [Fact (Nat.Prime p)] : (p * a).choose (p * b) ≡ a.choose b [MOD p]
• Choose.choose_modEq_choose_mod_mul_choose_div_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {n k p : ℕ} [Fact (Nat.Prime p)] : n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]
• Choose.choose_pow_mul_pow_mul_modEq_choose_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {k a b p : ℕ} [Fact (Nat.Prime p)] : (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]
• Choose.eq_pow_multiplicity_of_choose_modEq_zero_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {n p : ℕ} [Fact (Nat.Prime p)] (hn : 0 < n) (h : ∀ i ∈ Finset.Icc 1 (n - 1), n.choose i ≡ 0 [MOD p]) : n = p ^ multiplicity p n
• Choose.choose_modEq_prod_range_choose_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
• Choose.lucas_theorem_nat 📋 Mathlib.Data.Nat.Choose.Lucas
  {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
• Nat.modEq_nine_digits_sum 📋 Mathlib.Data.Nat.Digits.Div
  (n : ℕ) : n ≡ (Nat.digits 10 n).sum [MOD 9]
• Nat.modEq_three_digits_sum 📋 Mathlib.Data.Nat.Digits.Div
  (n : ℕ) : n ≡ (Nat.digits 10 n).sum [MOD 3]
• Nat.probablePrime_iff_modEq 📋 Mathlib.NumberTheory.FermatPsp
  (n : ℕ) {b : ℕ} (h : 1 ≤ b) : n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
• Pell.yn_modEq_two 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) (n : ℕ) : Pell.yn a1 n ≡ n [MOD 2]
• Pell.yn_modEq_a_sub_one 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) (n : ℕ) : Pell.yn a1 n ≡ n [MOD a - 1]
• Pell.xn_modEq_x4n_add 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) (n j : ℕ) : Pell.xn a1 (4 * n + j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
• Pell.xy_modEq_of_modEq 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a b c : ℕ} (a1 : 1 < a) (b1 : 1 < b) (h : a ≡ b [MOD c]) (n : ℕ) : Pell.xn a1 n ≡ Pell.xn b1 n [MOD c] ∧ Pell.yn a1 n ≡ Pell.yn b1 n [MOD c]
• Pell.xn_modEq_x2n_add 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) (n j : ℕ) : Pell.xn a1 (2 * n + j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
• Pell.xn_modEq_x2n_sub_lem 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ n) : Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
• Pell.xn_modEq_x4n_sub 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ 2 * n) : Pell.xn a1 (4 * n - j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
• Pell.xn_modEq_x2n_sub 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ 2 * n) : Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
• Pell.modEq_of_xn_modEq 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (ipos : 0 < i) (hin : i ≤ n) (h : Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n]) : j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n]
• Pell.eq_of_xn_modEq' 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n]) : j = i ∨ j + i = 4 * n
• Pell.eq_of_xn_modEq_le 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)) : i = j
• Pell.eq_of_xn_modEq 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (i2n : i ≤ 2 * n) (j2n : j ≤ 2 * n) (h : Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n]) (ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)) : i = j
• Pell.xy_modEq_yn 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a : ℕ} (a1 : 1 < a) (n k : ℕ) : Pell.xn a1 (n * k) ≡ Pell.xn a1 n ^ k [MOD Pell.yn a1 n ^ 2] ∧ Pell.yn a1 (n * k) ≡ k * Pell.xn a1 n ^ (k - 1) * Pell.yn a1 n [MOD Pell.yn a1 n ^ 3]
• Pell.eq_pow_of_pell 📋 Mathlib.NumberTheory.PellMatiyasevic
  {m n k : ℕ} : n ^ k = m ↔ k = 0 ∧ m = 1 ∨ 0 < k ∧ (n = 0 ∧ m = 0 ∨ 0 < n ∧ ∃ w a t z, ∃ (a1 : 1 < a), Pell.xn a1 k ≡ Pell.yn a1 k * (a - n) + m [MOD t] ∧ 2 * a * n = t + (n * n + 1) ∧ m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)
• Pell.matiyasevic 📋 Mathlib.NumberTheory.PellMatiyasevic
  {a k x y : ℕ} : (∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔ 1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ u v s t b, x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
• Dioph.modEq_dioph 📋 Mathlib.NumberTheory.Dioph
  {α : Type} {f g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {h : (α → ℕ) → ℕ} (dh : Dioph.DiophFn h) : Dioph {v | f v ≡ g v [MOD h v]}
• Nat.infinite_setOfPred_prime_and_modEq 📋 Mathlib.NumberTheory.LSeries.PrimesInAP
  {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) : {p | Nat.Prime p ∧ p ≡ a [MOD q]}.Infinite

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