multiplicity_eq_of_emultiplicity_eq_some

English

If emultiplicity a b = emultiplicity c d, then multiplicity a b = multiplicity c d.

Русский

Если emultiplicity a b = emultiplicity c d, то multiplicity a b = multiplicity c d.

LaTeX

$$$ \text{emultiplicity}(a,b) = \text{emultiplicity}(c,d) \Rightarrow \text{multiplicity}(a,b) = \text{multiplicity}(c,d) $$$

Lean4

theorem multiplicity_eq_of_emultiplicity_eq_some {n : ℕ} (h : emultiplicity a b = n) : multiplicity a b = n :=
  by
  simp [multiplicity, h]
  rfl

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