natCast_multiplicity — Mathlib

English

For natural numbers a,b, the multiplicity is preserved under casting to integers: multiplicity(a,b) = multiplicity(a,b) in integers.

Русский

Для натуральных a, b кратность сохраняется при приведении к целым: multiplicity (a:ℤ) (b:ℤ) = multiplicity a b.

LaTeX

$$$$multiplicity\ (a:\mathbb{Z})\ (b:\mathbb{Z}) = multiplicity\ a\ b.$$$$

Lean4

@[norm_cast]
theorem natCast_multiplicity (a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) = multiplicity a b :=
  multiplicity_eq_of_emultiplicity_eq (natCast_emultiplicity a b)

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