emultiplicity_eq_of_associated_left

English

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

Русский

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

LaTeX

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

Lean4

theorem emultiplicity_eq_of_associated_left {a b c : α} (h : Associated a b) : emultiplicity b c = emultiplicity a c :=
  le_antisymm (emultiplicity_le_emultiplicity_of_dvd_left h.dvd) (emultiplicity_le_emultiplicity_of_dvd_left h.symm.dvd)

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