emultiplicity_eq_multiplicity — Mathlib

English

For FiniteMultiplicity, emultiplicity a b equals multiplicity a b after casting to ENat.

Русский

Для FiniteMultiplicity emultiplicity a b равна кратности a b после приведения к ENat.

LaTeX

$$$ \text{FiniteMultiplicity}(a,b) \Rightarrow emultiplicity(a,b) = multiplicity(a,b).cast $$$

Lean4

theorem emultiplicity_eq_multiplicity (h : FiniteMultiplicity a b) : emultiplicity a b = multiplicity a b :=
  by
  cases hm : emultiplicity a b
  · simp [h] at hm
  rw [multiplicity_eq_of_emultiplicity_eq_some hm]

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