finiteMultiplicity_of_emultiplicity_eq_natCast

English

If emultiplicity a b equals a natural number n, then FiniteMultiplicity a b holds.

Русский

Если emultiplicity a b равно натуральному числу n, тогда FiniteMultiplicity a b выполняется.

LaTeX

$$$ emultiplicity(a,b) = n \Rightarrow FiniteMultiplicity(a,b) $$$

Lean4

theorem finiteMultiplicity_of_emultiplicity_eq_natCast {n : ℕ} (h : emultiplicity a b = n) : FiniteMultiplicity a b :=
  by
  by_contra nh
  rw [← emultiplicity_eq_top, h] at nh
  trivial

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