emultiplicity_natAbs — Mathlib

English

For every natural a and integer b, the emultiplicity of a with respect to |b| equals the emultiplicity of a viewed as an integer with b

Русский

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

LaTeX

$$$\\operatorname{emultiplicity}(a,|b|) = \\operatorname{emultiplicity}(a\\in\\mathbb{Z}, b)$$$

Lean4

theorem emultiplicity_natAbs (a : ℕ) (b : ℤ) : emultiplicity a b.natAbs = emultiplicity (a : ℤ) b :=
  by
  rcases Int.natAbs_eq b with h | h <;> conv_rhs => rw [h]
  · rw [Int.natCast_emultiplicity]
  · rw [emultiplicity_neg, Int.natCast_emultiplicity]

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