neg_mk

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.neg_mk

English

Negation commutes with mk: −mk(m, s) = mk(−m, s) for all m ∈ M and s ∈ ℕ+.

Русский

Отрицание commute с оператором mk: $-\\mathrm{mk}(m,s)=\\mathrm{mk}(-m,s)$.

LaTeX

$$$-\\mathrm{mk}(m,s) = \\mathrm{mk}(-m,s).$$$

Lean4

theorem neg_mk (m : M) (s : ℕ+) : -mk m s = mk (-m) s :=
  (eq_neg_of_add_eq_zero_left (by simp [mk_add_mk_left])).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru