Mathlib Map

Theorems · Theorem · commutative algebra

zero_notMem_nonZeroDivisorsLeft

∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], 0 ∉ nonZeroDivisorsLeft M₀
Defined in
Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Cited by
1 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext, Quot.sound
Assumes
MonoidWithZeroNontrivial
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

zero_notMem_nonZeroDivisors · cited by 6zero_notMem_nonZeroDiviso…Submonoid · cited by 3086SubmonoidNontrivial · cited by 2416NontrivialMulZeroClass.zero_mul · cited by 1625MulZeroClass.zero_mulone_ne_zero · cited by 885one_ne_zeroMonoidWithZero · cited by 456MonoidWithZerononZeroDivisorsLeft · cited by 26nonZeroDivisorsLeftzero_notMem_nonZeroDivisorsLe…CITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.