multiplicity_eq_of_associated_right

English

If b and c are associated, multiplicity a b = multiplicity a c.

Русский

Если b и c ассоциированы, умножимость a b равна умножимости a c.

LaTeX

$$$ \operatorname{multiplicity}(a,b) = \operatorname{multiplicity}(a,c) $$$

Lean4

theorem multiplicity_eq_of_associated_right {a b c : α} (h : Associated b c) : multiplicity a b = multiplicity a c :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_right h)

Похожие утверждения