multiplicity_eq_of_emultiplicity_eq

English

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

Русский

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

LaTeX

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

Lean4

theorem multiplicity_eq_of_emultiplicity_eq {c d : β} (h : emultiplicity a b = emultiplicity c d) :
    multiplicity a b = multiplicity c d := by
  unfold multiplicity
  rw [h]

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