multiplicity_eq_of_associated_left

English

If a and b are associated, then their multiplicities with respect to c are equal.

Русский

Если a и b ассоциированы, то их кратности по отношению к c равны.

LaTeX

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

Lean4

theorem multiplicity_eq_of_associated_left {a b c : α} (h : Associated a b) : multiplicity b c = multiplicity a c :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_left h)

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