Loogle!

Result

Found 653 declarations mentioning NoZeroDivisors. Of these, only the first 200 are shown.

NoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Defs
(M₀ : Type u_2) [Mul M₀] [Zero M₀] : Prop
IsLeftCancelMulZero.to_noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Defs
(M₀ : Type u_1) [MulZeroClass M₀] [IsLeftCancelMulZero M₀] : NoZeroDivisors M₀
IsRightCancelMulZero.to_noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Defs
(M₀ : Type u_1) [MulZeroClass M₀] [IsRightCancelMulZero M₀] : NoZeroDivisors M₀
mul_self_eq_zero 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : a * a = 0 ↔ a = 0
mul_self_ne_zero 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : a * a ≠ 0 ↔ a ≠ 0
zero_eq_mul_self 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : 0 = a * a ↔ a = 0
zero_ne_mul_self 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : 0 ≠ a * a ↔ a ≠ 0
NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_2} {inst✝ : Mul M₀} {inst✝¹ : Zero M₀} [self : NoZeroDivisors M₀] {a b : M₀} : a * b = 0 → a = 0 ∨ b = 0
NoZeroDivisors.mk 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_2} [Mul M₀] [Zero M₀] (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0) : NoZeroDivisors M₀
noZeroDivisors_iff 📋 Mathlib.Algebra.GroupWithZero.Defs
(M₀ : Type u_2) [Mul M₀] [Zero M₀] : NoZeroDivisors M₀ ↔ ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0
mul_eq_zero_comm 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ b * a = 0
mul_ne_zero_comm 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b ≠ 0 ↔ b * a ≠ 0
mul_eq_zero_iff_left 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) : a * b = 0 ↔ b = 0
mul_eq_zero_iff_right 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (hb : b ≠ 0) : a * b = 0 ↔ a = 0
mul_ne_zero_iff_left 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) : a * b ≠ 0 ↔ b ≠ 0
mul_ne_zero_iff_right 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (hb : b ≠ 0) : a * b ≠ 0 ↔ a ≠ 0
noZeroDivisors_iff_left_eq_zero_of_mul 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
noZeroDivisors_iff_right_eq_zero_of_mul 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0
mul_eq_zero 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ a = 0 ∨ b = 0
mul_ne_zero_iff 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
zero_eq_mul 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : 0 = a * b ↔ a = 0 ∨ b = 0
noZeroDivisors_iff_eq_zero_of_mul 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0
NeZero.mul 📋 Mathlib.Algebra.GroupWithZero.Basic
{M₀ : Type u_1} [Zero M₀] [Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y] : NeZero (x * y)
isReduced_of_noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Basic
{M₀ : Type u_1} [MonoidWithZero M₀] [NoZeroDivisors M₀] : IsReduced M₀
eq_zero_of_mul_self_eq_zero 📋 Mathlib.Algebra.GroupWithZero.Basic
{M₀ : Type u_1} [Mul M₀] [Zero M₀] [NoZeroDivisors M₀] {a : M₀} (h : a * a = 0) : a = 0
mul_ne_zero 📋 Mathlib.Algebra.GroupWithZero.Basic
{M₀ : Type u_1} [Mul M₀] [Zero M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0
MonoidWithZeroHom.one 📋 Mathlib.Algebra.GroupWithZero.Hom
(M₀ : Type u_7) (N₀ : Type u_8) [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] : One (M₀ →*₀ N₀)
MonoidWithZeroHom.one_apply_zero 📋 Mathlib.Algebra.GroupWithZero.Hom
{M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] : 1 0 = 0
MonoidWithZeroHom.one_apply_of_ne_zero 📋 Mathlib.Algebra.GroupWithZero.Hom
{M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] {x : M₀} (hx : x ≠ 0) : 1 x = 1
MonoidWithZeroHom.one_apply_eq_zero_iff 📋 Mathlib.Algebra.GroupWithZero.Hom
{M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} : 1 x = 0 ↔ x = 0
MonoidWithZeroHom.one_apply_eq_one_iff 📋 Mathlib.Algebra.GroupWithZero.Hom
{M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} : 1 x = 1 ↔ x ≠ 0
MonoidWithZeroHom.one_apply_def 📋 Mathlib.Algebra.GroupWithZero.Hom
{M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀) : 1 x = if x = 0 then 0 else 1
Function.Injective.noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.InjSurj
{M₀ : Type u_1} {M₀' : Type u_3} [Mul M₀] [Zero M₀] [Mul M₀'] [Zero M₀'] (f : M₀ → M₀') (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) [NoZeroDivisors M₀'] : NoZeroDivisors M₀
AddOpposite.instNoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Opposite
{α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ
MulOpposite.instNoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Opposite
{α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ
Subsingleton.to_noZeroDivisors 📋 Mathlib.Algebra.Ring.Basic
(α : Type u_3) [Mul α] [Zero α] [Subsingleton α] : NoZeroDivisors α
IsDomain.to_noZeroDivisors 📋 Mathlib.Algebra.Ring.Basic
(α : Type u_3) [Semiring α] [IsDomain α] : NoZeroDivisors α
NoZeroDivisors.to_isDomain 📋 Mathlib.Algebra.Ring.Basic
(α : Type u_3) [Ring α] [h : Nontrivial α] [NoZeroDivisors α] : IsDomain α
isDomain_iff_noZeroDivisors_and_nontrivial 📋 Mathlib.Algebra.Ring.Basic
(α : Type u_3) [Ring α] : IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
noZeroDivisors_iff_isDomain_or_subsingleton 📋 Mathlib.Algebra.Ring.Basic
(α : Type u_3) [Ring α] : NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
NoZeroDivisors.to_isCancelMulZero 📋 Mathlib.Algebra.Ring.Basic
(R : Type u_3) [NonUnitalNonAssocRing R] [NoZeroDivisors R] : IsCancelMulZero R
isCancelMulZero_iff_noZeroDivisors 📋 Mathlib.Algebra.Ring.Basic
{R : Type u_3} [NonUnitalNonAssocRing R] : IsCancelMulZero R ↔ NoZeroDivisors R
noZeroDivisors_tfae 📋 Mathlib.Algebra.Ring.Basic
{R : Type u_3} [NonUnitalNonAssocRing R] : [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE
GroupWithZero.noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Units.Basic
{G₀ : Type u_3} [GroupWithZero G₀] : NoZeroDivisors G₀
mul_self_eq_mul_self_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} : a * a = b * b ↔ a = b ∨ a = -b
Commute.mul_self_eq_mul_self_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R} (h : Commute a b) : a * a = b * b ↔ a = b ∨ a = -b
eq_or_eq_neg_of_sq_eq_sq 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [CommRing R] [NoZeroDivisors R] (a b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b
sq_eq_sq_iff_eq_or_eq_neg 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [CommRing R] [NoZeroDivisors R] {a b : R} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
sq_eq_one_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [Ring R] {a : R} [NoZeroDivisors R] : a ^ 2 = 1 ↔ a = 1 ∨ a = -1
sq_ne_one_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [Ring R] {a : R} [NoZeroDivisors R] : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1
Commute.sq_eq_sq_iff_eq_or_eq_neg 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [Ring R] {a b : R} [NoZeroDivisors R] (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
mul_self_eq_one_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [NonAssocRing R] [NoZeroDivisors R] {a : R} : a * a = 1 ↔ a = 1 ∨ a = -1
Units.inv_eq_self_iff 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1
Units.eq_or_eq_neg_of_sq_eq_sq 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [CommRing R] [NoZeroDivisors R] (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b
Units.sq_eq_sq_iff_eq_or_eq_neg 📋 Mathlib.Algebra.Ring.Commute
{R : Type u} [CommRing R] [NoZeroDivisors R] {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
sq_nonpos_iff 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] [NoZeroDivisors R] (r : R) : r ^ 2 ≤ 0 ↔ r = 0
eq_zero_of_mul_self_add_mul_self_eq_zero 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (h : a * a + b * b = 0) : a = 0
mul_self_add_mul_self_eq_zero 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] : a * a + b * b = 0 ↔ a = 0 ∧ b = 0
sq_add_sq_eq_zero 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] : a ^ 2 + b ^ 2 = 0 ↔ a = 0 ∧ b = 0
IsOrderedRing.toIsStrictOrderedRing 📋 Mathlib.Algebra.Order.Ring.Defs
(R : Type u_1) [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R] : IsStrictOrderedRing R
IsStrictOrderedRing.noZeroDivisors 📋 Mathlib.Algebra.Order.Ring.Defs
{R : Type u} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : NoZeroDivisors R
WithZero.instNoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.WithZero
{α : Type u_1} [Mul α] : NoZeroDivisors (WithZero α)
MonoidWithZeroHom.comp_one 📋 Mathlib.Algebra.GroupWithZero.WithZero
{M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun x => x = 0] (f : N₀ →*₀ G₀) : f.comp 1 = 1
MonoidWithZeroHom.one_apply_val_unit 📋 Mathlib.Algebra.GroupWithZero.WithZero
{M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MulZeroOneClass N₀] [DecidablePred fun x => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀ˣ) : 1 ↑x = 1
MonoidWithZeroHom.apply_one_apply_eq 📋 Mathlib.Algebra.GroupWithZero.WithZero
{M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun x => x = 0] (f : N₀ →*₀ G₀) (x : M₀) : f (1 x) = 1 x
pow_add_pow_eq_zero_iff_of_even 📋 Mathlib.Algebra.Order.Ring.Basic
{R : Type u_3} [Semiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] [NoZeroDivisors R] {n : ℕ} (hn : n ≠ 0) (hn' : Even n) (x y : R) : x ^ n + y ^ n = 0 ↔ x = 0 ∧ y = 0
mul_self_inj_of_nonneg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_3} [CommRing α] [NoZeroDivisors α] [PartialOrder α] [IsStrictOrderedRing α] {a b : α} (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b
CanonicallyOrderedAdd.mul_pos 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b
Nonneg.noZeroDivisors 📋 Mathlib.Algebra.Order.Nonneg.Ring
{α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [NoZeroDivisors α] : NoZeroDivisors (Nonneg α)
MulEquiv.noZeroDivisors 📋 Mathlib.Algebra.Ring.Equiv
{A : Type u_7} (B : Type u_8) [MulZeroClass A] [MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B) : NoZeroDivisors A
MulEquiv.noZeroDivisors_iff 📋 Mathlib.Algebra.Ring.Equiv
{A : Type u_7} {B : Type u_8} [MulZeroClass A] [MulZeroClass B] (e : A ≃* B) : NoZeroDivisors A ↔ NoZeroDivisors B
Lex.instNoZeroDivisors 📋 Mathlib.Algebra.Order.GroupWithZero.Synonym
{α : Type u_1} [Mul α] [Zero α] [NoZeroDivisors α] : NoZeroDivisors (Lex α)
OrderDual.instNoZeroDivisors 📋 Mathlib.Algebra.Order.GroupWithZero.Synonym
{α : Type u_1} [Mul α] [Zero α] [NoZeroDivisors α] : NoZeroDivisors αᵒᵈ
WithBot.instSemigroupWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithBot α)
WithTop.instSemigroupWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α)
WithBot.instMonoidWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : MonoidWithZero (WithBot α)
WithTop.instMonoidWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : MonoidWithZero (WithTop α)
WithBot.instNoZeroDivisors 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] : NoZeroDivisors (WithBot α)
WithTop.instNoZeroDivisors 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] : NoZeroDivisors (WithTop α)
WithBot.instCommMonoidWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithBot α)
WithTop.instCommMonoidWithZero 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithTop α)
WithBot.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [NonUnitalSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] : NonUnitalSemiring (WithBot α)
WithBot.instSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [Semiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] [Nontrivial α] : Semiring (WithBot α)
WithTop.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [NonUnitalSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] : NonUnitalSemiring (WithTop α)
WithTop.instSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [Semiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] [Nontrivial α] : Semiring (WithTop α)
WithBot.instCommSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] [Nontrivial α] : CommSemiring (WithBot α)
WithTop.instCommSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] [Nontrivial α] : CommSemiring (WithTop α)
WithBot.eq_bot_of_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} (n : ℕ) (hx : x ^ n = ⊥) : x = ⊥
WithBot.pow_ne_bot 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} {n : ℕ} (hx : x ≠ ⊥) : x ^ n ≠ ⊥
WithTop.eq_top_of_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} (n : ℕ) (hx : x ^ n = ⊤) : x = ⊤
WithTop.pow_ne_top 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} (hx : x ≠ ⊤) : x ^ n ≠ ⊤
WithBot.bot_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} (hn : n ≠ 0) : ⊥ ^ n = ⊥
WithTop.top_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} (hn : n ≠ 0) : ⊤ ^ n = ⊤
WithBot.coe_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) : ↑(a ^ n) = ↑a ^ n
WithTop.coe_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) : ↑(a ^ n) = ↑a ^ n
WithBot.pow_eq_bot_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} {n : ℕ} : x ^ n = ⊥ ↔ x = ⊥ ∧ n ≠ 0
WithBot.pow_ne_bot_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} {n : ℕ} : x ^ n ≠ ⊥ ↔ x ≠ ⊥ ∨ n = 0
WithTop.pow_eq_top_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} : x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
WithTop.pow_ne_top_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} : x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
WithTop.instIsOrderedRing 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithTop α)
WithBot.bot_lt_pow 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} {n : ℕ} [Preorder α] (hx : ⊥ < x) : ⊥ < x ^ n
WithTop.pow_lt_top 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} [Preorder α] (hx : x < ⊤) : x ^ n < ⊤
WithBot.instIsOrderedRing 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithBot α)
WithBot.bot_lt_pow_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithBot α} {n : ℕ} [Preorder α] : ⊥ < x ^ n ↔ ⊥ < x ∨ n = 0
WithTop.pow_lt_top_iff 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} [Preorder α] : x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
WithTop.pow_right_strictMono 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [OrderBot α] [CanonicallyOrderedAdd α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} : n ≠ 0 → StrictMono fun a => a ^ n
WithTop.pow_lt_pow_left 📋 Mathlib.Algebra.Order.Ring.WithTop
{α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [OrderBot α] [CanonicallyOrderedAdd α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {a b : WithTop α} (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n
instNoZeroDivisorsENat 📋 Mathlib.Data.ENat.Monoid
: NoZeroDivisors ℕ∞
Cardinal.noZeroDivisors 📋 Mathlib.SetTheory.Cardinal.Order
: NoZeroDivisors Cardinal.{u}
add_self_eq_zero 📋 Mathlib.Algebra.Ring.CharZero
{R : Type u_2} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} : a + a = 0 ↔ a = 0
CharZero.eq_neg_self_iff 📋 Mathlib.Algebra.Ring.CharZero
{R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : a = -a ↔ a = 0
CharZero.neg_eq_self_iff 📋 Mathlib.Algebra.Ring.CharZero
{R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : -a = a ↔ a = 0
nat_mul_inj' 📋 Mathlib.Algebra.Ring.CharZero
{R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) (w : n ≠ 0) : a = b
nat_mul_inj 📋 Mathlib.Algebra.Ring.CharZero
{R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) : n = 0 ∨ a = b
NonUnitalSubsemiringClass.noZeroDivisors 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
{R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) [NoZeroDivisors R] : NoZeroDivisors ↥s
SubsemiringClass.noZeroDivisors 📋 Mathlib.Algebra.Ring.Subsemiring.Defs
{R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [NoZeroDivisors R] : NoZeroDivisors ↥s
Subsemiring.noZeroDivisors 📋 Mathlib.Algebra.Ring.Subsemiring.Defs
{R : Type u} [NonAssocSemiring R] (s : Subsemiring R) [NoZeroDivisors R] : NoZeroDivisors ↥s
Subring.instNoZeroDivisorsSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
{R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors ↥s
NoZeroDivisors.of_faithfulSMul 📋 Mathlib.Algebra.Algebra.Basic
(R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [NoZeroDivisors A] : NoZeroDivisors R
Associates.instNoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Associated
{M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] : NoZeroDivisors (Associates M)
coe_nonZeroDivisorsLeft_eq 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
(M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
coe_nonZeroDivisorsRight_eq 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
(M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}
mem_nonZeroDivisors_of_ne_zero 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) : x ∈ nonZeroDivisors M₀
noZeroDivisors_iff_forall_mem_nonZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisors M₀
noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisorsLeft M₀
noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisorsRight M₀
mem_nonZeroDivisors_iff_ne_zero 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] [Nontrivial M₀] : x ∈ nonZeroDivisors M₀ ↔ x ≠ 0
powers_le_nonZeroDivisors_of_noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) : Submonoid.powers x ≤ nonZeroDivisors M₀
eq_zero_of_ne_zero_of_mul_left_eq_zero 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) (hxy : x * y = 0) : y = 0
eq_zero_of_ne_zero_of_mul_right_eq_zero 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) (hxy : y * x = 0) : y = 0
le_nonZeroDivisors_of_noZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{M₀ : Type u_2} [MonoidWithZero M₀] [NoZeroDivisors M₀] {S : Submonoid M₀} (hS : 0 ∉ S) : S ≤ nonZeroDivisors M₀
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Function.Injective ⇑f) : nonZeroDivisors M₀ ≤ Submonoid.comap f (nonZeroDivisors M₀')
map_mem_nonZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F) (hg : Function.Injective ⇑g) {x : M₀} (h : x ∈ nonZeroDivisors M₀) : g x ∈ nonZeroDivisors M₀'
map_le_nonZeroDivisors_of_injective 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
{F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Function.Injective ⇑f) {S : Submonoid M₀} (hS : S ≤ nonZeroDivisors M₀) : Submonoid.map f S ≤ nonZeroDivisors M₀'
Set.instNoZeroDivisors 📋 Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
{α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α)
Finset.prod_ne_zero_iff 📋 Mathlib.Algebra.BigOperators.GroupWithZero.Finset
{ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀] [NoZeroDivisors M₀] : ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0
Finset.prod_eq_zero_iff 📋 Mathlib.Algebra.BigOperators.GroupWithZero.Finset
{ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀] [NoZeroDivisors M₀] : ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0
Finset.support_prod 📋 Mathlib.Algebra.BigOperators.GroupWithZero.Finset
{ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] (s : Finset ι) (f : ι → κ → M₀) : (Function.support fun j => ∏ i ∈ s, f i j) = ⋂ i ∈ s, Function.support (f i)
List.prod_eq_zero_iff 📋 Mathlib.Algebra.BigOperators.Ring.List
{M₀ : Type u_4} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {l : List M₀} : l.prod = 0 ↔ 0 ∈ l
List.prod_ne_zero 📋 Mathlib.Algebra.BigOperators.Ring.List
{M₀ : Type u_4} [MonoidWithZero M₀] {l : List M₀} [Nontrivial M₀] [NoZeroDivisors M₀] (hL : 0 ∉ l) : l.prod ≠ 0
Multiset.prod_eq_zero_iff 📋 Mathlib.Algebra.BigOperators.Ring.Multiset
{M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀} : s.prod = 0 ↔ 0 ∈ s
Multiset.prod_ne_zero 📋 Mathlib.Algebra.BigOperators.Ring.Multiset
{M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀} (h : 0 ∉ s) : s.prod ≠ 0
Finsupp.prod_ne_zero_iff 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
{α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β} : f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
Finsupp.prod_eq_zero_iff 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
{α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β} : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
Function.support_mul 📋 Mathlib.Algebra.GroupWithZero.Indicator
{ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀) : (Function.support fun x => f x * g x) = Function.support f ∩ Function.support g
Function.support_mul_of_ne_zero_left 📋 Mathlib.Algebra.GroupWithZero.Indicator
{ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] {f : ι → M₀} (hf : ∀ (x : ι), f x ≠ 0) (g : ι → M₀) : (Function.support fun x => f x * g x) = Function.support g
Function.support_mul_of_ne_zero_right 📋 Mathlib.Algebra.GroupWithZero.Indicator
{ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) {g : ι → M₀} (hg : ∀ (x : ι), g x ≠ 0) : (Function.support fun x => f x * g x) = Function.support f
Function.support_mul' 📋 Mathlib.Algebra.GroupWithZero.Indicator
{ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀) : Function.support (f * g) = Function.support f ∩ Function.support g
AbsoluteValue.trivial 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_4} [Semiring R] [DecidablePred fun x => x = 0] [NoZeroDivisors R] {S : Type u_5} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Nontrivial S] : AbsoluteValue R S
IsAbsoluteValue.abv_neg 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S] [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a : R) : abv (-a) = abv a
AbsoluteValue.isNontrivial_iff_ne_trivial 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_4} [Semiring R] {S : Type u_5} [Semiring S] [PartialOrder S] [IsOrderedRing S] [DecidablePred fun x => x = 0] [NoZeroDivisors R] [Nontrivial S] (v : AbsoluteValue R S) : v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial
AbsoluteValue.addGroupSeminormClass 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] : AddGroupSeminormClass (AbsoluteValue R S) R S
AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S
IsAbsoluteValue.abv_sub 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S] [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a b : R) : abv (a - b) = abv (b - a)
AbsoluteValue.trivial_apply 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_4} [Semiring R] [DecidablePred fun x => x = 0] [NoZeroDivisors R] {S : Type u_5} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Nontrivial S] {x : R} (hx : x ≠ 0) : AbsoluteValue.trivial x = 1
AbsoluteValue.map_neg 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R) : abv (-a) = abv a
AbsoluteValue.apply_natAbs_eq 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (x : ℤ) : abv ↑x.natAbs = abv ↑x
AbsoluteValue.map_sub 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R) : abv (a - b) = abv (b - a)
AbsoluteValue.le_add 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R) : abv a - abv b ≤ abv (a + b)
AbsoluteValue.sub_le_add 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R) : abv (a - b) ≤ abv a + abv b
AbsoluteValue.eq_on_nat_iff_eq_on_int 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
{R : Type u_2} {S : Type u_3} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] {f g : AbsoluteValue R S} : (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n
CanonicallyOrderedAdd.list_prod_pos 📋 Mathlib.Algebra.Order.BigOperators.Ring.List
{α : Type u_2} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] {l : List α} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x
CanonicallyOrderedAdd.multiset_prod_pos 📋 Mathlib.Algebra.Order.BigOperators.Ring.Multiset
{R : Type u_1} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x
Mathlib.Meta.Positivity.prod_ne_zero 📋 Mathlib.Algebra.Order.BigOperators.Ring.Finset
{ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀] [NoZeroDivisors M₀] : (∀ a ∈ s, f a ≠ 0) → ∏ x ∈ s, f x ≠ 0
CanonicallyOrderedAdd.prod_pos 📋 Mathlib.Algebra.Order.BigOperators.Ring.Finset
{ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] {f : ι → R} {s : Finset ι} [NoZeroDivisors R] [Nontrivial R] : 0 < ∏ i ∈ s, f i ↔ ∀ i ∈ s, 0 < f i
finsum_mul 📋 Mathlib.Algebra.BigOperators.Finprod
{α : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R) : (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
mul_finsum 📋 Mathlib.Algebra.BigOperators.Finprod
{α : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R) : r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
finprod_ne_zero 📋 Mathlib.Algebra.BigOperators.Finprod
{α : Type u_1} {M₀ : Type u_7} [CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {f : α → M₀} (h : ∀ (i : α), f i ≠ 0) : ∏ᶠ (i : α), f i ≠ 0
finprod_apply_ne_zero 📋 Mathlib.Algebra.BigOperators.Finprod
{ι : Type u_7} {N₀ : Type u_8} {M₀ : Type u_9} [CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {n : N₀} {f : ι → N₀ → M₀} (h : ∀ (i : ι), f i n ≠ 0) : (∏ᶠ (i : ι), f i) n ≠ 0
finsum_mem_mul 📋 Mathlib.Algebra.BigOperators.Finprod
{α : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R) : (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r
mul_finsum_mem 📋 Mathlib.Algebra.BigOperators.Finprod
{α : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R) : r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
Ideal.isPrime_bot 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.IsPrime
Ideal.primeCompl_bot 📋 Mathlib.RingTheory.Ideal.Prime
{α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.primeCompl = nonZeroDivisors α
Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors 📋 Mathlib.RingTheory.Ideal.Maximal
{α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] [NoZeroDivisors α] [Nontrivial α] {P : Ideal α} : P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = Ideal.span {p}
Ideal.Quotient.noZeroDivisors 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
{R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I)
NoZeroDivisors.toNoZeroSMulDivisors 📋 Mathlib.Algebra.NoZeroSMulDivisors.Defs
{R : Type u_1} [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R
Ordinal.noZeroDivisors 📋 Mathlib.SetTheory.Ordinal.Arithmetic
: NoZeroDivisors Ordinal.{u_4}
DFinsupp.prod_ne_zero_iff 📋 Mathlib.Data.DFinsupp.BigOperators
{ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} : f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
DFinsupp.prod_eq_zero_iff 📋 Mathlib.Data.DFinsupp.BigOperators
{ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums 📋 Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
{R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors (AddMonoidAlgebra R A)
MonoidAlgebra.instNoZeroDivisorsOfUniqueProds 📋 Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
{R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Mul A] [UniqueProds A] : NoZeroDivisors (MonoidAlgebra R A)
Polynomial.instNoZeroDivisors 📋 Mathlib.Algebra.Polynomial.Basic
{R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Polynomial R)
Polynomial.noZeroDivisors_iff 📋 Mathlib.Algebra.Polynomial.Basic
{R : Type u} [Semiring R] : NoZeroDivisors (Polynomial R) ↔ NoZeroDivisors R
AlgHom.eq_piEvalAlgHom 📋 Mathlib.LinearAlgebra.StdBasis
{k : Type u_1} {G : Type u_2} [CommSemiring k] [NoZeroDivisors k] [Nontrivial k] [Finite G] (φ : (G → k) →ₐ[k] k) : ∃ s, φ = Pi.evalAlgHom k (fun i => k) s
SetSemiring.instNoZeroDivisors 📋 Mathlib.Data.Set.Semiring
{α : Type u_1} [Mul α] : NoZeroDivisors (SetSemiring α)
Submodule.instNoZeroDivisors 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] [NoZeroDivisors A] : NoZeroDivisors (Submodule R A)
Submodule.mul_eq_bot 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] [NoZeroDivisors A] {M N : Submodule R A} : M * N = ⊥ ↔ M = ⊥ ∨ N = ⊥
Ideal.isRadical_bot_of_noZeroDivisors 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u_2} [CommSemiring R] [NoZeroDivisors R] : ⊥.IsRadical
Ideal.primeCompl_le_nonZeroDivisors 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u_1} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] : P.primeCompl ≤ nonZeroDivisors R
Ideal.inf_ne_bot_of_ne_bot 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [Semiring R] [NoZeroDivisors R] {I J : Ideal R} [I.IsTwoSided] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊓ J ≠ ⊥
Ideal.mul_eq_bot 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [Semiring R] {I J : Ideal R} [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥
Ideal.span_singleton_nonZeroDivisors 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {r : R} : Ideal.span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R
Matrix.vecMulVec_ne_zero 📋 Mathlib.Data.Matrix.Mul
{n : Type u_3} {α : Type v} [Mul α] [Zero α] [NoZeroDivisors α] {a b : n → α} (ha : a ≠ 0) (hb : b ≠ 0) : Matrix.vecMulVec a b ≠ 0
Matrix.vecMulVec_eq_zero 📋 Mathlib.Data.Matrix.Mul
{n : Type u_3} {α : Type v} [MulZeroClass α] [NoZeroDivisors α] {a b : n → α} : Matrix.vecMulVec a b = 0 ↔ a = 0 ∨ b = 0
NonUnitalSubalgebra.noZeroDivisors 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
{R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] (S : NonUnitalSubalgebra R A) : NoZeroDivisors ↥S
Subalgebra.noZeroDivisors 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
{R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [NoZeroDivisors A] [Algebra R A] (S : Subalgebra R A) : NoZeroDivisors ↥S
Submonoid.LocalizationMap.noZeroDivisors 📋 Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
{M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) [NoZeroDivisors M] : NoZeroDivisors N
OreLocalization.instGroupWithZeroNonZeroDivisors 📋 Mathlib.RingTheory.OreLocalization.NonZeroDivisors
{R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : GroupWithZero (OreLocalization (nonZeroDivisors R) R)
OreLocalization.inv' 📋 Mathlib.RingTheory.OreLocalization.NonZeroDivisors
{R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : Inv (OreLocalization (nonZeroDivisors R) R)
OreLocalization.instCommGroupWithZeroNonZeroDivisors 📋 Mathlib.RingTheory.OreLocalization.NonZeroDivisors
{R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : CommGroupWithZero (OreLocalization (nonZeroDivisors R) R)

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:

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.
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