Mathlib Map

Theorems · Theorem · commutative algebra

not_addIrreducible_zero

∀ {M : Type u_1} [inst : AddMonoid M], ¬AddIrreducible 0
Defined in
Mathlib.Algebra.Group.Irreducible.Defs
Cited by
3 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

addIrreducible_mem_addSubmonoidClosure_subset · cited by 2addIrreducible_mem_addSub…not_addIrreducible_nsmul · cited by 1not_addIrreducible_nsmulAddIrreducible.ne_zero · cited by 0AddIrreducible.ne_zeroAddMonoid · cited by 2864AddMonoidIsAddUnit · cited by 215IsAddUnitAddIrreducible · cited by 24AddIrreducibleaddIrreducible_iff · cited by 6addIrreducible_iffisAddUnit_zero · cited by 5isAddUnit_zeronot_addIrreducible_zeroCITED BYCITES

Cites5

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

Cited by3

Results whose statement or proof uses this declaration.