Theorems · Theorem · group theory

mul_eq_zero

∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0

If α has no zero divisors, then the product of two elements equals zero iff one of them equals zero.

Defined in

Mathlib.Algebra.GroupWithZero.Defs

Cited by

94 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 22 definitions · uses no axioms

Assumes

MulZeroClassNoZeroDivisors