multiplicity_natAbs — Mathlib

English

For every natural a and integer b, the multiplicity of a with respect to b.natAbs equals the multiplicity of a cast to integers with b

Русский

Для любого натурального a и целого b кратность a по отношению к b.natAbs равна кратности a, приведённому к целым, по отношению к b.

LaTeX

$$$\\operatorname{multiplicity}(a, b\\mathrm{.natAbs}) = \\operatorname{multiplicity}(\\, (a:\\mathbb{Z}) , b)$$$

Lean4

theorem multiplicity_natAbs (a : ℕ) (b : ℤ) : multiplicity a b.natAbs = multiplicity (a : ℤ) b :=
  multiplicity_eq_of_emultiplicity_eq (Int.emultiplicity_natAbs a b)

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