emultiplicity_eq_iff_multiplicity_eq

English

If FiniteMultiplicity a b, then emultiplicity a b = n cast iff multiplicity a b = n.

Русский

Если FiniteMultiplicity a b, то emultiplicity a b = n cast эквивалентна multiplicity a b = n.

LaTeX

$$∀ {n}, (FiniteMultiplicity a b) → (emultiplicity a b = n.cast ↔ multiplicity a b = n)$$

Lean4

theorem emultiplicity_eq_iff_multiplicity_eq {n : ℕ} (h : FiniteMultiplicity a b) :
    emultiplicity a b = n ↔ multiplicity a b = n := by simp [h.emultiplicity_eq_multiplicity]

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