Mathlib Map

Theorems · Theorem · commutative algebra

multiplicity_of_isUnit_right

∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, ¬IsUnit a → IsUnit b → multiplicity a b = 0
Defined in
Mathlib.RingTheory.Multiplicity
Cited by
2 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

multiplicity_of_one_right · cited by 1multiplicity_of_one_rightmultiplicity_of_unit_right · cited by 0multiplicity_of_unit_rightCommMonoid · cited by 2264CommMonoidIsUnit · cited by 1602IsUnitmultiplicity · cited by 117multiplicityisUnit_of_dvd_unit · cited by 22isUnit_of_dvd_unitmultiplicity_eq_zero · cited by 3multiplicity_eq_zeromultiplicity_of_isUnit_rightCITED BYCITES

Cites5

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

Cited by2

Results whose statement or proof uses this declaration.