emultiplicity_eq_iff_multiplicity_eq_of_ne_one

English

For n ≠ 1, emultiplicity a b = n.cast iff multiplicity a b = n.

Русский

Для n ≠ 1, emultiplicity a b = n.cast эквивалентно multiplicity a b = n.

LaTeX

$$$ n \neq 1 \Rightarrow (emultiplicity(a,b) = n.cast \iff multiplicity(a,b) = n) $$$

Lean4

theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_one {n : ℕ} (h : n ≠ 1) :
    emultiplicity a b = n ↔ multiplicity a b = n := by
  constructor
  · exact multiplicity_eq_of_emultiplicity_eq_some
  · intro h₂
    simpa [multiplicity, WithTop.untopD_eq_iff, h] using h₂

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