Loogle!

Result

Found 1812 declarations mentioning Nat.Prime. Of these, 153 have a name containing "iff".

• Nat.irreducible_iff_nat_prime 📋 Mathlib.Data.Nat.Prime.Defs
  (a : ℕ) : Irreducible a ↔ Nat.Prime a
• Nat.prime_iff 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ Prime p
• Nat.Prime.coprime_iff_not_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {p n : ℕ} (pp : Nat.Prime p) : p.Coprime n ↔ ¬p ∣ n
• Nat.prime_dvd_prime_iff_eq 📋 Mathlib.Data.Nat.Prime.Defs
  {p q : ℕ} (pp : Nat.Prime p) (qp : Nat.Prime q) : p ∣ q ↔ p = q
• Nat.not_prime_iff_minFac_lt 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (n2 : 2 ≤ n) : ¬Nat.Prime n ↔ n.minFac < n
• char_eq_expChar_iff 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [AddMonoidWithOne R] (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ Nat.Prime p
• CharP.charP_iff_prime_eq_zero 📋 Mathlib.Algebra.CharP.Basic
  {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : ℕ} (hp : Nat.Prime p) : CharP R p ↔ ↑p = 0
• CharZero.charZero_iff_forall_prime_ne_zero 📋 Mathlib.Algebra.CharP.Basic
  (R : Type u_1) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
• Nat.Prime.dvd_iff_not_coprime 📋 Mathlib.Data.Nat.Prime.Basic
  {p n : ℕ} (pp : Nat.Prime p) : p ∣ n ↔ ¬p.Coprime n
• Nat.Prime.even_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : Even p ↔ p = 2
• Nat.eq_one_iff_not_exists_prime_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n = 1 ↔ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ n
• Nat.ne_one_iff_exists_prime_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n ≠ 1 ↔ ∃ p, Nat.Prime p ∧ p ∣ n
• Nat.Prime.dvd_iff_eq 📋 Mathlib.Data.Nat.Prime.Basic
  {p a : ℕ} (hp : Nat.Prime p) (a1 : a ≠ 1) : a ∣ p ↔ p = a
• Nat.Prime.not_coprime_iff_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {m n : ℕ} : ¬m.Coprime n ↔ ∃ p, Nat.Prime p ∧ p ∣ m ∧ p ∣ n
• Nat.Prime.mod_two_eq_one_iff_ne_two 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} [Fact (Nat.Prime p)] : p % 2 = 1 ↔ p ≠ 2
• Nat.Prime.pow_eq_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p a k : ℕ} (hp : Nat.Prime p) : a ^ k = p ↔ a = p ∧ k = 1
• Nat.not_prime_iff_exists_dvd_ne 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
• Nat.prime_mul_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {a b : ℕ} : Nat.Prime (a * b) ↔ Nat.Prime a ∧ b = 1 ∨ Nat.Prime b ∧ a = 1
• Nat.not_prime_iff_exists_dvd_lt 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
• Nat.Prime.mul_eq_prime_sq_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {x y p : ℕ} (hp : Nat.Prime p) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p
• Function.minimalPeriod_eq_prime_iff 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.minimalPeriod f x = p ↔ Function.IsPeriodicPt f p x ∧ ¬Function.IsFixedPt f x
• isPrimePow_nat_iff 📋 Mathlib.Algebra.IsPrimePow
  (n : ℕ) : IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
• isPrimePow_nat_iff_bounded 📋 Mathlib.Algebra.IsPrimePow
  (n : ℕ) : IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
• Nat.mem_primeFactorsList_iff_dvd 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) : p ∈ n.primeFactorsList ↔ p ∣ n
• Nat.replicate_subperm_primeFactorsList_iff 📋 Mathlib.Data.Nat.Factors
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : (List.replicate n a).Subperm b.primeFactorsList ↔ a ^ n ∣ b
• Nat.sum_properDivisors_eq_one_iff_prime 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : ∑ x ∈ n.properDivisors, x = 1 ↔ Nat.Prime n
• Nat.properDivisors_eq_singleton_one_iff_prime 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : n.properDivisors = {1} ↔ Nat.Prime n
• addOrderOf_eq_prime_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : addOrderOf x = p ↔ p • x = 0 ∧ x ≠ 0
• orderOf_eq_prime_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
• exists_addOrderOf_eq_prime_pow_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, addOrderOf x = p ^ k) ↔ ∃ m, p ^ m • x = 0
• exists_orderOf_eq_prime_pow_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, orderOf x = p ^ k) ↔ ∃ m, x ^ p ^ m = 1
• ZMod.isUnit_prime_iff_not_dvd 📋 Mathlib.Data.ZMod.Basic
  {n p : ℕ} (hp : Nat.Prime p) : IsUnit ↑p ↔ ¬p ∣ n
• Nat.Prime.dvd_choose_pow_iff 📋 Mathlib.Data.Nat.Multiplicity
  {p n k : ℕ} (hp : Nat.Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n
• Nat.Prime.pow_dvd_factorial_iff 📋 Mathlib.Data.Nat.Multiplicity
  {p n r b : ℕ} (hp : Nat.Prime p) (hbn : Nat.log p n < b) : p ^ r ∣ n.factorial ↔ r ≤ ∑ i ∈ Finset.Ico 1 b, n / p ^ i
• Equiv.Perm.pow_prime_eq_one_iff 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)] : σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p
• le_padicValNat_iff_replicate_subperm_primeFactorsList 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList
• le_emultiplicity_iff_replicate_subperm_primeFactorsList 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList
• Nat.factorization_eq_zero_iff 📋 Mathlib.Data.Nat.Factorization.Defs
  (n p : ℕ) : n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
• Nat.eq_iff_prime_padicValNat_eq 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a = b ↔ ∀ (p : ℕ), Nat.Prime p → padicValNat p a = padicValNat p b
• Nat.dvd_iff_prime_pow_dvd_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (n d : ℕ) : d ∣ n ↔ ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ d → p ^ k ∣ n
• Nat.Prime.dvd_iff_one_le_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {p n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ∣ n ↔ 1 ≤ n.factorization p
• Nat.Prime.pow_dvd_iff_le_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p
• Nat.factorization_eq_zero_iff_remainder 📋 Mathlib.Data.Nat.Factorization.Basic
  {p r : ℕ} (i : ℕ) (pp : Nat.Prime p) (hr0 : r ≠ 0) : ¬p ∣ r ↔ (p * i + r).factorization p = 0
• Nat.factorization_prime_le_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : (∀ (p : ℕ), Nat.Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n
• Nat.eq_factorization_iff 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Nat.Prime p) : f = n.factorization ↔ (f.prod fun x1 x2 => x1 ^ x2) = n
• Nat.Prime.pow_dvd_iff_dvd_ordProj 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
• Nat.Prime.pow_dvd_iff_dvd_ord_proj 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
• Nat.totient_eq_iff_prime 📋 Mathlib.Data.Nat.Totient
  {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ Nat.Prime p
• Nat.prime_iff_card_units 📋 Mathlib.Data.Nat.Totient
  (p : ℕ) [Fintype (ZMod p)ˣ] : Nat.Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
• AddMonoid.exponent_eq_prime_iff 📋 Mathlib.GroupTheory.Exponent
  {G : Type u_1} [AddMonoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : AddMonoid.exponent G = p ↔ ∀ (g : G), g ≠ 0 → addOrderOf g = p
• Monoid.exponent_eq_prime_iff 📋 Mathlib.GroupTheory.Exponent
  {G : Type u_1} [Monoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : Monoid.exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
• AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {α : Type u_1} [Finite α] [AddCommGroup α] : IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Nat.card α)
• CommGroup.is_simple_iff_isCyclic_and_prime_card 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {α : Type u_1} [Finite α] [CommGroup α] : IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Nat.card α)
• not_isAddCyclic_iff_exponent_eq_prime 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {α : Type u_1} [AddGroup α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) : ¬IsAddCyclic α ↔ AddMonoid.exponent α = p
• not_isCyclic_iff_exponent_eq_prime 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {α : Type u_1} [Group α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) : ¬IsCyclic α ↔ Monoid.exponent α = p
• IsPGroup.iff_card 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite G] : IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
• IsPGroup.iff_orderOf 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] : IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
• IsPGroup.nontrivial_iff_card 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] [Finite G] : Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n
• prime_dvd_char_iff_dvd_card 📋 Mathlib.Algebra.CharP.CharAndCard
  {R : Type u_1} [CommRing R] [Fintype R] (p : ℕ) [Fact (Nat.Prime p)] : p ∣ ringChar R ↔ p ∣ Fintype.card R
• isUnit_iff_not_dvd_char 📋 Mathlib.Algebra.CharP.CharAndCard
  (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Finite R] : IsUnit ↑p ↔ ¬p ∣ ringChar R
• isUnit_iff_not_dvd_char_of_ringChar_ne_zero 📋 Mathlib.Algebra.CharP.CharAndCard
  (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] (hR : ringChar R ≠ 0) : IsUnit ↑p ↔ ¬p ∣ ringChar R
• CharP.isUnit_natCast_iff 📋 Mathlib.Algebra.CharP.Invertible
  {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} (hp : Nat.Prime p) : IsUnit ↑n ↔ ¬p ∣ n
• CharP.isUnit_intCast_iff 📋 Mathlib.Algebra.CharP.Invertible
  {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {z : ℤ} (hp : Nat.Prime p) : IsUnit ↑z ↔ ¬↑p ∣ z
• CharP.isUnit_ofNat_iff 📋 Mathlib.Algebra.CharP.Invertible
  {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} [n.AtLeastTwo] (hp : Nat.Prime p) : IsUnit (OfNat.ofNat n) ↔ ¬p ∣ OfNat.ofNat n
• X_pow_sub_C_irreducible_iff_of_prime 📋 Mathlib.FieldTheory.KummerPolynomial
  {K : Type u} [Field K] {p : ℕ} (hp : Nat.Prime p) {a : K} : Irreducible (Polynomial.X ^ p - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
• isPrimePow_iff_unique_prime_dvd 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} : IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
• exists_ordCompl_eq_one_iff_isPrimePow 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• exists_ord_compl_eq_one_iff_isPrimePow 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• Nat.squarefree_and_prime_pow_iff_prime 📋 Mathlib.Data.Nat.Squarefree
  {n : ℕ} : Squarefree n ∧ IsPrimePow n ↔ Nat.Prime n
• Nat.squarefree_iff_prime_squarefree 📋 Mathlib.Data.Nat.Squarefree
  {n : ℕ} : Squarefree n ↔ ∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ n
• Nat.Squarefree.ext_iff 📋 Mathlib.Data.Nat.Squarefree
  {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : n = m ↔ ∀ (p : ℕ), Nat.Prime p → (p ∣ n ↔ p ∣ m)
• ArithmeticFunction.cardFactors_eq_one_iff_prime 📋 Mathlib.NumberTheory.ArithmeticFunction
  {n : ℕ} : ArithmeticFunction.cardFactors n = 1 ↔ Nat.Prime n
• ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers 📋 Mathlib.NumberTheory.ArithmeticFunction
  {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) (g : ArithmeticFunction R) (hg : g.IsMultiplicative) : f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
• Nat.prime_iff_prime_int 📋 Mathlib.Data.Nat.Prime.Int
  {p : ℕ} : Nat.Prime p ↔ Prime ↑p
• Int.prime_ofNat_iff 📋 Mathlib.Data.Nat.Prime.Int
  {n : ℕ} : Prime (OfNat.ofNat n) ↔ Nat.Prime (OfNat.ofNat n)
• Int.prime_iff_natAbs_prime 📋 Mathlib.RingTheory.Int.Basic
  {k : ℤ} : Prime k ↔ Nat.Prime k.natAbs
• mem_bot_iff_intCast 📋 Mathlib.FieldTheory.Finite.Basic
  (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_4) [DivisionRing K] [CharP K p] {x : K} : x ∈ ⊥ ↔ ∃ n, ↑n = x
• Subfield.mem_bot_iff_pow_eq_self 📋 Mathlib.FieldTheory.Finite.Basic
  (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {x : F} : x ∈ ⊥ ↔ x ^ p = x
• padicValRat.finite_int_prime_iff 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ} : FiniteMultiplicity (↑p) a ↔ a ≠ 0
• dvd_iff_padicValNat_ne_zero 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p n : ℕ} [Fact (Nat.Prime p)] (hn0 : n ≠ 0) : p ∣ n ↔ padicValNat p n ≠ 0
• padicValNat_dvd_iff_le 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p : ℕ} [hp : Fact (Nat.Prime p)] {a n : ℕ} (ha : a ≠ 0) : p ^ n ∣ a ↔ n ≤ padicValNat p a
• padicValNat_dvd_iff 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
• padicValInt_dvd_iff 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ) : ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
• nat_log_eq_padicValNat_iff 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : 0 < n) : Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)
• padicValRat.padicValRat_le_padicValRat_iff 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p : ℕ} [hp : Fact (Nat.Prime p)] {n₁ n₂ d₁ d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) : padicValRat p (Rat.divInt n₁ d₁) ≤ padicValRat p (Rat.divInt n₂ d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
• Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
  {m k p : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] [hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R} [NeZero ↑m] : (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
• IsUnit.natCast_factorial_iff_of_charP 📋 Mathlib.Data.Nat.Factorial.NatCast
  {A : Type u_1} [Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p] {n : ℕ} : IsUnit ↑n.factorial ↔ n < p
• ZMod.eq_zero_iff_gcd_ne_one 📋 Mathlib.Data.ZMod.Coprime
  {a : ℤ} {p : ℕ} [pp : Fact (Nat.Prime p)] : ↑a = 0 ↔ a.gcd ↑p ≠ 1
• FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize 📋 Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
  {φ : FirstOrder.Language.ring.Sentence} : FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Infinite
• FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize 📋 Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
  {φ : FirstOrder.Language.ring.Sentence} : FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}ᶜ.Finite
• Cardinal.nat_is_prime_iff 📋 Mathlib.SetTheory.Cardinal.Divisibility
  {n : ℕ} : Prime ↑n ↔ Nat.Prime n
• Cardinal.is_prime_iff 📋 Mathlib.SetTheory.Cardinal.Divisibility
  {a : Cardinal.{u_1}} : Prime a ↔ Cardinal.aleph0 ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
• PerfectClosure.r_iff 📋 Mathlib.FieldTheory.PerfectClosure
  (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (a✝ a✝¹ : ℕ × K) : PerfectClosure.R K p a✝ a✝¹ ↔ ∃ n x, a✝ = (n, x) ∧ a✝¹ = (n + 1, (frobenius K p) x)
• PerfectClosure.natCast_eq_iff 📋 Mathlib.FieldTheory.PerfectClosure
  (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ) : ↑x = ↑y ↔ ↑x = ↑y
• PerfectClosure.mk_eq_iff 📋 Mathlib.FieldTheory.PerfectClosure
  (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
• PerfectClosure.eq_iff 📋 Mathlib.FieldTheory.PerfectClosure
  (K : Type u) [CommRing K] [IsReduced K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔ (⇑(frobenius K p))^[y.1] x.2 = (⇑(frobenius K p))^[x.1] y.2
• X_pow_sub_C_irreducible_iff_forall_prime_of_odd 📋 Mathlib.FieldTheory.KummerExtension
  {K : Type u} [Field K] {n : ℕ} (hn : Odd n) {a : K} : Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
• X_pow_sub_C_irreducible_iff_of_prime_pow 📋 Mathlib.FieldTheory.KummerExtension
  {K : Type u} [Field K] {p : ℕ} (hp : Nat.Prime p) (hp' : p ≠ 2) {n : ℕ} (hn : n ≠ 0) {a : K} : Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
• isZGroup_iff 📋 Mathlib.GroupTheory.SpecificGroups.ZGroup
  (G : Type u_1) [Group G] : IsZGroup G ↔ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
• padicNorm.nat_eq_one_iff 📋 Mathlib.NumberTheory.Padics.PadicNorm
  {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicNorm p ↑m = 1 ↔ ¬p ∣ m
• padicNorm.nat_lt_one_iff 📋 Mathlib.NumberTheory.Padics.PadicNorm
  {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicNorm p ↑m < 1 ↔ p ∣ m
• padicNorm.int_eq_one_iff 📋 Mathlib.NumberTheory.Padics.PadicNorm
  {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ) : padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
• padicNorm.int_lt_one_iff 📋 Mathlib.NumberTheory.Padics.PadicNorm
  {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ) : padicNorm p ↑m < 1 ↔ ↑p ∣ m
• padicNorm.dvd_iff_norm_le 📋 Mathlib.NumberTheory.Padics.PadicNorm
  {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)
• Padic.norm_le_one_iff_val_nonneg 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) : ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
• padicNormE.norm_int_lt_one_iff_dvd 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) : ‖↑k‖ < 1 ↔ ↑p ∣ k
• PadicSeq.norm_zero_iff 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) : f.norm = 0 ↔ f ≈ 0
• Padic.norm_le_pow_iff_norm_lt_pow_add_one 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ) : ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
• Padic.norm_lt_pow_iff_norm_le_pow_sub_one 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ) : ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
• padicNormE.norm_int_le_pow_iff_dvd 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) (n : ℕ) : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
• PadicSeq.val_eq_iff_norm_eq 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [Fact (Nat.Prime p)] {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) : f.valuation = g.valuation ↔ f.norm = g.norm
• PadicSeq.eq_zero_iff_equiv_zero 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p) : CauSeq.Completion.mk f = 0 ↔ f ≈ 0
• PadicSeq.ne_zero_iff_nequiv_zero 📋 Mathlib.NumberTheory.Padics.PadicNumbers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p) : CauSeq.Completion.mk f ≠ 0 ↔ ¬f ≈ 0
• PadicInt.isUnit_iff 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : IsUnit z ↔ ‖z‖ = 1
• PadicInt.not_isUnit_iff 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : ¬IsUnit z ↔ ‖z‖ < 1
• PadicInt.norm_int_lt_one_iff_dvd 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) : ‖↑k‖ < 1 ↔ ↑p ∣ k
• PadicInt.mem_subring_iff 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  (p : ℕ) [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} : x ∈ PadicInt.subring p ↔ ‖x‖ ≤ 1
• PadicInt.norm_le_pow_iff_norm_lt_pow_add_one 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ) : ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
• PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ) : ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
• PadicInt.norm_int_le_pow_iff_dvd 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℤ} {n : ℕ} : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
• PadicInt.norm_lt_one_iff_dvd 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ‖x‖ < 1 ↔ ↑p ∣ x
• PadicInt.norm_le_pow_iff_le_valuation 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation
• PadicInt.pow_p_dvd_int_iff 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ) : ↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a
• PadicInt.norm_le_pow_iff_mem_span_pow 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
• PadicInt.mem_span_pow_iff_le_valuation 📋 Mathlib.NumberTheory.Padics.PadicIntegers
  {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation
• PadicInt.toZModPow_eq_iff_ext 📋 Mathlib.NumberTheory.Padics.RingHoms
  {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {g g' : R →+* ℤ_[p]} : (∀ (n : ℕ), (PadicInt.toZModPow n).comp g = (PadicInt.toZModPow n).comp g') ↔ g = g'
• Nat.mem_smoothNumbers_iff_forall_le 📋 Mathlib.NumberTheory.SmoothNumbers
  {n m : ℕ} : m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p < n
• Nat.mem_factoredNumbers_iff_forall_le 📋 Mathlib.NumberTheory.SmoothNumbers
  {s : Finset ℕ} {m : ℕ} : m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p ∈ s
• legendreSym.eq_neg_one_iff 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} : legendreSym p a = -1 ↔ ¬IsSquare ↑a
• legendreSym.eq_zero_iff 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : legendreSym p a = 0 ↔ ↑a = 0
• legendreSym.eq_neg_one_iff' 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} : legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
• legendreSym.eq_neg_one_iff_not_one 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha : ↑a ≠ 0) : legendreSym p a = -1 ↔ ¬legendreSym p a = 1
• ZMod.exists_sq_eq_neg_one_iff 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  {p : ℕ} [Fact (Nat.Prime p)] : IsSquare (-1) ↔ p % 4 ≠ 3
• legendreSym.eq_one_iff 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha0 : ↑a ≠ 0) : legendreSym p a = 1 ↔ IsSquare ↑a
• legendreSym.eq_one_iff' 📋 Mathlib.NumberTheory.LegendreSymbol.Basic
  (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} (ha0 : ↑a ≠ 0) : legendreSym p ↑a = 1 ↔ IsSquare ↑a
• FiniteField.isSquare_odd_prime_iff 📋 Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
  {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
• ZMod.exists_sq_eq_two_iff 📋 Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
  {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7
• ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one 📋 Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
  {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp1 : p % 4 = 1) (hq1 : q ≠ 2) : IsSquare ↑q ↔ IsSquare ↑p
• ZMod.exists_sq_eq_neg_two_iff 📋 Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
  {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
• ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three 📋 Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
  {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp3 : p % 4 = 3) (hq3 : q % 4 = 3) (hpq : p ≠ q) : IsSquare ↑q ↔ ¬IsSquare ↑p
• lucas_primality_iff 📋 Mathlib.NumberTheory.LucasPrimality
  (p : ℕ) : Nat.Prime p ↔ ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
• ZMod.nonsquare_iff_jacobiSym_eq_neg_one 📋 Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
  {a : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : jacobiSym a p = -1 ↔ ¬IsSquare ↑a
• PadicInt.fwdDiff_mahlerSeries 📋 Mathlib.NumberTheory.Padics.MahlerBasis
  {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (n : ℕ) : (fwdDiff 1)^[n] (⇑(PadicInt.mahlerSeries a)) 0 = a n
• PadicInt.fwdDiff_tendsto_zero 📋 Mathlib.NumberTheory.Padics.MahlerBasis
  {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)) : Filter.Tendsto (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0)
• PadicInt.fwdDiff_iter_le_of_forall_le 📋 Mathlib.NumberTheory.Padics.MahlerBasis
  {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] {f : C(ℤ_[p], E)} {s t : ℕ} (hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s) (n : ℕ) : ‖(fwdDiff 1)^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s
• GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime 📋 Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
  (p : ℕ) [Fact (Nat.Prime p)] : Prime ↑p ↔ p % 4 = 3
• Nat.eq_sq_add_sq_iff 📋 Mathlib.NumberTheory.SumTwoSquares
  {n : ℕ} : (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Nat.Prime q → q % 4 = 3 → Even (padicValNat q n)
• ZMod.isSquare_neg_one_iff 📋 Mathlib.NumberTheory.SumTwoSquares
  {n : ℕ} (hn : Squarefree n) : IsSquare (-1) ↔ ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
• Nat.prime_iff_fac_equiv_neg_one 📋 Mathlib.NumberTheory.Wilson
  {n : ℕ} (h : n ≠ 1) : Nat.Prime n ↔ ↑(n - 1).factorial = -1
• Perfection.ext_iff 📋 Mathlib.RingTheory.Perfection
  {R : Type u₁} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {f g : Ring.Perfection R p} : f = g ↔ ∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g
• WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero 📋 Mathlib.RingTheory.WittVector.Complete
  {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] {x y : WittVector p k} {n : ℕ} : (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0
• WittVector.mem_span_p_iff_coeff_zero_eq_zero 📋 Mathlib.RingTheory.WittVector.Complete
  {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) : x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0
• WittVector.mem_span_p_pow_iff_le_coeff_eq_zero 📋 Mathlib.RingTheory.WittVector.Complete
  {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) (n : ℕ) : x ∈ Ideal.span {↑p ^ n} ↔ ∀ m < n, x.coeff m = 0

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65