Theorems · Theorem · group theory

mul_ne_zero_iff

∀ {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 is nonzero iff both of them are nonzero.

Defined in

Mathlib.Algebra.GroupWithZero.Defs

Cited by

39 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

MulZeroClassNoZeroDivisors