emultiplicity_mk_eq_emultiplicity

English

The emultiplicity between the associate classes of a and b equals the emultiplicity of a and b themselves.

Русский

Эмплитичность между классами ассоциаций a и b равна эмплитичности a и b сами по себе.

LaTeX

$$$\\operatorname{emultiplicity}(\\mathrm{Associates}(a), \\mathrm{Associates}(b)) = \\operatorname{emultiplicity}(a,b)$$$

Lean4

theorem emultiplicity_mk_eq_emultiplicity {a b : α} :
    emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b := by
  simp [emultiplicity_eq_emultiplicity_iff, ← Associates.mk_pow, Associates.mk_dvd_mk]

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