Loogle!

Result

Found 2181 declarations whose name contains "prime". Of these, 330 have a name containing "prime" and "iff". Of these, only the first 200 are shown.

Nat.coprime_iff_gcd_eq_one 📋 Batteries.Data.Nat.Gcd
{m n : ℕ} : m.Coprime n ↔ m.gcd n = 1
Nat.coprime_mul_iff_left 📋 Batteries.Data.Nat.Gcd
{m n k : ℕ} : (m * n).Coprime k ↔ m.Coprime k ∧ n.Coprime k
Nat.coprime_mul_iff_right 📋 Batteries.Data.Nat.Gcd
{k m n : ℕ} : k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime n
IsRelPrime.mul_left_iff 📋 Mathlib.Algebra.Divisibility.Units
{α : Type u_1} [CommMonoid α] {x y z : α} [DecompositionMonoid α] : IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z
IsRelPrime.mul_right_iff 📋 Mathlib.Algebra.Divisibility.Units
{α : Type u_1} [CommMonoid α] {x y z : α} [DecompositionMonoid α] : IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z
irreducible_iff_prime 📋 Mathlib.Algebra.Prime.Defs
{M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a
Prime.dvd_pow_iff_dvd 📋 Mathlib.Algebra.Prime.Defs
{M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a
MulEquiv.prime_iff 📋 Mathlib.Algebra.Prime.Lemmas
{M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {p : M} {E : Type u_5} [EquivLike E M N] [MulEquivClass E M N] (e : E) : Prime (e p) ↔ Prime p
Associated.prime_iff 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) : Prime p ↔ Prime q
Irreducible.isRelPrime_iff_not_dvd 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) : IsRelPrime p n ↔ ¬p ∣ n
Associates.mk_isRelPrime_iff 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CommMonoid M] {a b : M} : IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
prime_pow_iff 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {n : ℕ} : Prime (p ^ n) ↔ Prime p ∧ n = 1
Prime.dvd_prime_iff_associated 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ Associated p q
prime_dvd_prime_iff_eq 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_2} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ p = q
prime_mul_iff 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CancelCommMonoidWithZero M] {x y : M} : Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Associates.irreducible_iff_prime_iff 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CommMonoidWithZero M] : (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
associates_irreducible_iff_prime 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {p : Associates M} : Irreducible p ↔ Prime p
pow_eq_pow_iff_of_coprime 📋 Mathlib.Data.Int.GCD
{α : Type u_1} [CommGroupWithZero α] {a b : α} {m n : ℕ} (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
Commute.pow_eq_pow_iff_of_coprime 📋 Mathlib.Data.Int.GCD
{α : Type u_1} [GroupWithZero α] {a b : α} {m n : ℕ} (hab : Commute a b) (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
Nat.isCoprime_iff 📋 Mathlib.RingTheory.Coprime.Basic
{m n : ℕ} : IsCoprime m n ↔ m = 1 ∨ n = 1
IsCoprime.neg_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] (x y : R) : IsCoprime (-x) y ↔ IsCoprime x y
IsCoprime.neg_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] (x y : R) : IsCoprime x (-y) ↔ IsCoprime x y
PNat.isCoprime_iff 📋 Mathlib.RingTheory.Coprime.Basic
{m n : ℕ+} : IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1
IsCoprime.mul_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommSemiring R] {x y z : R} : IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z
IsCoprime.mul_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommSemiring R] {x y z : R} : IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
IsRelPrime.neg_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] (x y : R) : IsRelPrime (-x) y ↔ IsRelPrime x y
IsRelPrime.neg_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] (x y : R) : IsRelPrime x (-y) ↔ IsRelPrime x y
IsCoprime.neg_neg_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] (x y : R) : IsCoprime (-x) (-y) ↔ IsCoprime x y
Semifield.isCoprime_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [Semifield R] {m n : R} : IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
IsCoprime.add_mul_left_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime (x + y * z) y ↔ IsCoprime x y
IsCoprime.add_mul_left_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime x (y + x * z) ↔ IsCoprime x y
IsCoprime.add_mul_right_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime (x + z * y) y ↔ IsCoprime x y
IsCoprime.add_mul_right_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime x (y + z * x) ↔ IsCoprime x y
IsCoprime.mul_add_left_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime (y * z + x) y ↔ IsCoprime x y
IsCoprime.mul_add_left_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime x (x * z + y) ↔ IsCoprime x y
IsCoprime.mul_add_right_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime (z * y + x) y ↔ IsCoprime x y
IsCoprime.mul_add_right_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] {x y z : R} : IsCoprime x (z * x + y) ↔ IsCoprime x y
IsCoprime.abs_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) : IsCoprime |x| y ↔ IsCoprime x y
IsCoprime.abs_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) : IsCoprime x |y| ↔ IsCoprime x y
IsRelPrime.neg_neg_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] (x y : R) : IsRelPrime (-x) (-y) ↔ IsRelPrime x y
IsRelPrime.add_mul_left_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime (x + y * z) y ↔ IsRelPrime x y
IsRelPrime.add_mul_left_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime x (y + x * z) ↔ IsRelPrime x y
IsRelPrime.add_mul_right_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime (x + z * y) y ↔ IsRelPrime x y
IsRelPrime.add_mul_right_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime x (y + z * x) ↔ IsRelPrime x y
IsRelPrime.mul_add_left_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime (y * z + x) y ↔ IsRelPrime x y
IsRelPrime.mul_add_left_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime x (x * z + y) ↔ IsRelPrime x y
IsRelPrime.mul_add_right_left_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime (z * y + x) y ↔ IsRelPrime x y
IsRelPrime.mul_add_right_right_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u_1} [CommRing R] {x y z : R} : IsRelPrime x (z * x + y) ↔ IsRelPrime x y
IsCoprime.abs_abs_iff 📋 Mathlib.RingTheory.Coprime.Basic
{R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) : IsCoprime |x| |y| ↔ IsCoprime x y
Nat.isCoprime_iff_coprime 📋 Mathlib.RingTheory.Coprime.Lemmas
{m n : ℕ} : IsCoprime ↑m ↑n ↔ m.Coprime n
Int.isCoprime_iff_gcd_eq_one 📋 Mathlib.RingTheory.Coprime.Lemmas
{m n : ℤ} : IsCoprime m n ↔ m.gcd n = 1
IsCoprime.prod_left_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
IsCoprime.prod_right_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} : IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)
IsCoprime.pow_left_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (hm : 0 < m) : IsCoprime (x ^ m) y ↔ IsCoprime x y
IsCoprime.pow_right_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (hm : 0 < m) : IsCoprime x (y ^ m) ↔ IsCoprime x y
IsRelPrime.prod_left_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
IsRelPrime.prod_right_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} : IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
IsRelPrime.pow_left_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ} (hm : 0 < m) : IsRelPrime (x ^ m) y ↔ IsRelPrime x y
IsRelPrime.pow_right_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ} (hm : 0 < m) : IsRelPrime x (y ^ m) ↔ IsRelPrime x y
IsCoprime.pow_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} [CommSemiring R] {x y : R} {m n : ℕ} (hm : 0 < m) (hn : 0 < n) : IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y
IsRelPrime.pow_iff 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : ℕ} (hm : 0 < m) (hn : 0 < n) : IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y
pairwise_coprime_iff_coprime_prod 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] : Pairwise (Function.onFun IsCoprime fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
exists_sum_eq_one_iff_pairwise_coprime' 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} {I : Type v} [CommSemiring R] {s : I → R} [Fintype I] [Nonempty I] [DecidableEq I] : (∃ μ, ∑ i, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (Function.onFun IsCoprime s)
pairwise_isRelPrime_iff_isRelPrime_prod 📋 Mathlib.RingTheory.Coprime.Lemmas
{α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {s : I → α} {t : Finset I} [DecidableEq I] : Pairwise (Function.onFun IsRelPrime fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
exists_sum_eq_one_iff_pairwise_coprime 📋 Mathlib.RingTheory.Coprime.Lemmas
{R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] (h : t.Nonempty) : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (Function.onFun IsCoprime fun i => s ↑i)
Ideal.IsPrime.pow_mem_iff_mem 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I
Ideal.IsPrime.mul_mem_iff_mem_or_mem 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) {x y : α} : x * y ∈ I ↔ x ∈ I ∨ y ∈ I
Ideal.isPrime_iff 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] {I : Ideal α} : I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
Ideal.not_isPrime_iff 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] {I : Ideal α} : ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
Ring.not_isField_iff_exists_prime 📋 Mathlib.RingTheory.Ideal.Basic
{R : Type u_5} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime
Ideal.isCoprime_span_singleton_iff 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] (x y : R) : IsCoprime (Ideal.span {x}) (Ideal.span {y}) ↔ IsCoprime x y
Ideal.sup_eq_top_iff_isCoprime 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u_2} [CommSemiring R] (x y : R) : Ideal.span {x} ⊔ Ideal.span {y} = ⊤ ↔ IsCoprime x y
Ideal.isCoprime_iff_codisjoint 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ Codisjoint I J
Ideal.isCoprime_iff_sup_eq 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I ⊔ J = ⊤
Ideal.IsPrime.multiset_prod_mem_iff_exists_mem 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Multiset R) : s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
Ideal.IsPrime.prod_mem_iff_exists_mem 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Finset R) : ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
Ideal.isCoprime_iff_add 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I + J = 1
Ideal.IsPrime.prod_mem_iff 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] : ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p
Ideal.IsPrime.radical_le_iff 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsPrime) : I.radical ≤ J ↔ I ≤ J
Ideal.isCoprime_iff_exists 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Ideal.IsPrime.pow_le_iff 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ P ↔ I ≤ P
Ideal.comap_map_eq_self_iff_of_isPrime 📋 Mathlib.RingTheory.Ideal.Maps
{R : Type u} [CommSemiring R] {S : Type u_2} [CommSemiring S] {f : R →+* S} (p : Ideal R) [p.IsPrime] : Ideal.comap f (Ideal.map f p) = p ↔ ∃ q, q.IsPrime ∧ Ideal.comap f q = p
Ideal.disjoint_map_primeCompl_iff_comap_le 📋 Mathlib.RingTheory.Ideal.Maps
{R : Type u} [CommSemiring R] {S : Type u_2} [Semiring S] {f : R →+* S} {p : Ideal R} {I : Ideal S} [p.IsPrime] : Disjoint ↑I ↑(Submonoid.map f p.primeCompl) ↔ Ideal.comap f I ≤ p
Nat.coprime_one_left_iff 📋 Mathlib.Data.Nat.GCD.Basic
(n : ℕ) : Nat.Coprime 1 n ↔ True
Nat.coprime_one_right_iff 📋 Mathlib.Data.Nat.GCD.Basic
(n : ℕ) : n.Coprime 1 ↔ True
Nat.coprime_iff_isRelPrime 📋 Mathlib.Data.Nat.GCD.Basic
{m n : ℕ} : m.Coprime n ↔ IsRelPrime m n
Nat.add_coprime_iff_left 📋 Mathlib.Data.Nat.GCD.Basic
{a b c : ℕ} (h : c ∣ b) : (a + b).Coprime c ↔ a.Coprime c
Nat.add_coprime_iff_right 📋 Mathlib.Data.Nat.GCD.Basic
{a b c : ℕ} (h : c ∣ a) : (a + b).Coprime c ↔ b.Coprime c
Nat.coprime_add_iff_left 📋 Mathlib.Data.Nat.GCD.Basic
{a b c : ℕ} (h : a ∣ c) : a.Coprime (b + c) ↔ a.Coprime b
Nat.coprime_add_iff_right 📋 Mathlib.Data.Nat.GCD.Basic
{a b c : ℕ} (h : a ∣ b) : a.Coprime (b + c) ↔ a.Coprime c
Nat.coprime_pow_left_iff 📋 Mathlib.Data.Nat.GCD.Basic
{n : ℕ} (hn : 0 < n) (a b : ℕ) : (a ^ n).Coprime b ↔ a.Coprime b
Nat.coprime_pow_right_iff 📋 Mathlib.Data.Nat.GCD.Basic
{n : ℕ} (hn : 0 < n) (a b : ℕ) : a.Coprime (b ^ n) ↔ a.Coprime b
Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime 📋 Mathlib.Data.Nat.GCD.Basic
{x n m : ℕ} (hcop : n.Coprime m) : x.gcd n * x.gcd m = x ↔ x ∣ n * m
Ideal.Quotient.isDomain_iff_prime 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
{R : Type u} [Ring R] (I : Ideal R) [I.IsTwoSided] : IsDomain (R ⧸ I) ↔ I.IsPrime
gcd_isUnit_iff_isRelPrime 📋 Mathlib.Algebra.GCDMonoid.Basic
{α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {a b : α} : IsUnit (gcd a b) ↔ IsRelPrime a b
UniqueFactorizationMonoid.irreducible_iff_prime 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Defs
{α : Type u_2} {inst✝ : CancelCommMonoidWithZero α} [self : UniqueFactorizationMonoid α] {a : α} : Irreducible a ↔ Prime a
UniqueFactorizationMonoid.exists_prime_iff 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Defs
{α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : (∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x
Irreducible.coprime_iff_not_dvd 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) : IsCoprime p n ↔ ¬p ∣ n
Irreducible.dvd_iff_not_coprime 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n
Irreducible.dvd_iff_not_isCoprime 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n
Prime.coprime_iff_not_dvd 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {p n : R} (hp : Prime p) : IsCoprime p n ↔ ¬p ∣ n
isRelPrime_iff_isCoprime 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] : IsRelPrime x y ↔ IsCoprime x y
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.irreducible_iff_prime 📋 Mathlib.Data.Nat.Prime.Defs
{p : ℕ} : Irreducible 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
Polynomial.prime_C_iff 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [CommRing R] {r : R} : Prime (Polynomial.C r) ↔ Prime r
MvPolynomial.prime_C_iff 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} (σ : Type v) [CommRing R] {r : R} : Prime (MvPolynomial.C r) ↔ Prime r
Ideal.isPrime_map_C_iff_isPrime 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [CommRing R] (P : Ideal R) : (Ideal.map Polynomial.C P).IsPrime ↔ P.IsPrime
MvPolynomial.prime_rename_iff 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} {σ : Type v} [CommRing R] (s : Set σ) {p : MvPolynomial (↑s) R} : Prime ((MvPolynomial.rename Subtype.val) p) ↔ 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_iff_pow_succ 📋 Mathlib.Algebra.IsPrimePow
{R : Type u_1} [CommMonoidWithZero R] (n : R) : IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
isPrimePow_nat_iff_bounded 📋 Mathlib.Algebra.IsPrimePow
(n : ℕ) : IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Prime.dvd_prod_iff 📋 Mathlib.Data.List.Prime
{M : Type u_1} [CommMonoidWithZero M] {p : M} {L : List M} (pp : Prime p) : p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a
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.mem_primeFactors_iff_mem_primeFactorsList 📋 Mathlib.Data.Nat.PrimeFin
{n p : ℕ} : p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
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_iff_coprime 📋 Mathlib.Data.ZMod.Basic
(m n : ℕ) : IsUnit ↑m ↔ m.Coprime n
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
Prime.dvd_finset_prod_iff 📋 Mathlib.Algebra.BigOperators.Associated
{α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {S : Finset α} {p : M} (pp : Prime p) (g : α → M) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
Prime.dvd_finsuppProd_iff 📋 Mathlib.Algebra.BigOperators.Associated
{α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) : p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a)
Prime.dvd_finsupp_prod_iff 📋 Mathlib.Algebra.BigOperators.Associated
{α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) : p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a)
Nat.coprime_multiset_prod_left_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{m : Multiset ℕ} {k : ℕ} : m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k
Nat.coprime_multiset_prod_right_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{k : ℕ} {m : Multiset ℕ} : k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n
Nat.coprime_list_prod_left_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{l : List ℕ} {k : ℕ} : l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
Nat.coprime_list_prod_right_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{k : ℕ} {l : List ℕ} : k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n
Nat.coprime_fintype_prod_left_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{ι : Type u_1} [Fintype ι] {s : ι → ℕ} {x : ℕ} : (∏ i, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x
Nat.coprime_fintype_prod_right_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{ι : Type u_1} [Fintype ι] {x : ℕ} {s : ι → ℕ} : x.Coprime (∏ i, s i) ↔ ∀ (i : ι), x.Coprime (s i)
Nat.coprime_prod_left_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ} : (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x
Nat.coprime_prod_right_iff 📋 Mathlib.Data.Nat.GCD.BigOperators
{ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ} : x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s 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.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_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.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
ExpChar.pow_prime_pow_mul_eq_one_iff 📋 Mathlib.Algebra.CharP.Reduced
{R : Type u_1} [CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] (x : R) : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
mem_rootsOfUnity_prime_pow_mul_iff 📋 Mathlib.RingTheory.RootsOfUnity.Basic
(R : Type u_4) [CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : Rˣ} : ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R
mem_rootsOfUnity_prime_pow_mul_iff' 📋 Mathlib.RingTheory.RootsOfUnity.Basic
(R : Type u_4) [CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : Rˣ} : ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R
UniqueFactorizationMonoid.iff_exists_prime_factors 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Basic
{α : Type u_1} [CancelCommMonoidWithZero α] : UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Basic
{R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) : IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d
irreducible_iff_prime_of_exists_prime_factors 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Basic
{α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a) {p : α} : Irreducible p ↔ Prime p
irreducible_iff_prime_of_existsUnique_irreducible_factors 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Basic
{α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) (p : α) : Irreducible p ↔ Prime p
irreducible_iff_prime_of_exists_unique_irreducible_factors 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Basic
{α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) (p : α) : Irreducible p ↔ Prime p
IsLocalization.isPrime_iff_isPrime_disjoint 📋 Mathlib.RingTheory.Localization.Ideal
{R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (J : Ideal S) : J.IsPrime ↔ (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
Ideal.minimalPrimes_eq_empty_iff 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
{R : Type u_1} [CommSemiring R] (I : Ideal R) : I.minimalPrimes = ∅ ↔ I = ⊤
Ideal.IsPrime.smul_iff 📋 Mathlib.RingTheory.Ideal.Pointwise
{M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {I : Ideal R} (g : M) : (g • I).IsPrime ↔ I.IsPrime
PrimeSpectrum.ext_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
{R : Type u_1} {inst✝ : CommSemiring R} {x y : PrimeSpectrum R} : x = y ↔ x.asIdeal = y.asIdeal
IsLocalization.AtPrime.isUnit_to_map_iff 📋 Mathlib.RingTheory.Localization.AtPrime
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) : IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl
IsLocalization.AtPrime.isUnit_mk'_iff 📋 Mathlib.RingTheory.Localization.AtPrime
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) : IsUnit (IsLocalization.mk' S x y) ↔ x ∈ I.primeCompl
IsLocalization.AtPrime.to_map_mem_maximal_iff 📋 Mathlib.RingTheory.Localization.AtPrime
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (h : IsLocalRing S := ⋯) : (algebraMap R S) x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
IsLocalization.AtPrime.mk'_mem_maximal_iff 📋 Mathlib.RingTheory.Localization.AtPrime
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) (h : IsLocalRing S := ⋯) : IsLocalization.mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
Localization.le_comap_primeCompl_iff 📋 Mathlib.RingTheory.Localization.AtPrime
{R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] {I : Ideal R} [hI : I.IsPrime] {J : Ideal P} [J.IsPrime] {f : R →+* P} : I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I
nilpotent_iff_mem_prime 📋 Mathlib.RingTheory.Nilpotent.Lemmas
{R : Type u_1} [CommSemiring R] {x : R} : IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
PrimeSpectrum.isMax_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] {x : PrimeSpectrum R} : IsMax x ↔ x.asIdeal.IsMaximal
PrimeSpectrum.zeroLocus_diff_singleton_zero 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] (s : Set R) : PrimeSpectrum.zeroLocus (s \ {0}) = PrimeSpectrum.zeroLocus s
PrimeSpectrum.isMin_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] {x : PrimeSpectrum R} : IsMin x ↔ x.asIdeal ∈ minimalPrimes R
PrimeSpectrum.zeroLocus_eq_top_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] (s : Set R) : PrimeSpectrum.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical R)
PrimeSpectrum.zeroLocus_eq_univ_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] (s : Set R) : PrimeSpectrum.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical R)
PrimeSpectrum.vanishingIdeal_eq_top_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : PrimeSpectrum.vanishingIdeal s = ⊤ ↔ s = ∅
PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
(R : Type u) [CommSemiring R] (t : Set (PrimeSpectrum R)) (s : Set R) : t ⊆ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑(PrimeSpectrum.vanishingIdeal t)
PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] {f : R} {I : PrimeSpectrum R} : I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal
PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
{R : Type u} [CommSemiring R] (f g : R) : PrimeSpectrum.zeroLocus {f} ⊆ PrimeSpectrum.zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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