natCast_emultiplicity — Mathlib

English

For natural numbers a,b, the emultiplicity is unchanged by casting to integers: emultiplicity(a,b) in integers equals emultiplicity(a,b).

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem natCast_emultiplicity (a b : ℕ) : emultiplicity (a : ℤ) (b : ℤ) = emultiplicity a b :=
  by
  unfold emultiplicity FiniteMultiplicity
  congr! <;> norm_cast

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