multiplicity_neg — Mathlib

English

For all a,b in α, the multiplicity of a with respect to −b equals the multiplicity of a with respect to b

Русский

Пусть a,b ∈ α. Кратность a по отношению к −b равна кратности a по отношению к b.

LaTeX

$$$\\operatorname{multiplicity}(a,-b) = \\operatorname{multiplicity}(a,b)$$$

Lean4

@[simp]
theorem multiplicity_neg (a b : α) : multiplicity a (-b) = multiplicity a b :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_neg a b)

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