toMul_neg

Mathlib.Algebra.Group.TypeTags.Basic

URI: https://scilib.ai/kg/mathlib#toMul_neg

English

For every x in Additive α, the multiplicative image of the additive negation equals the multiplicative inverse: (−x)^{Mul} = (x^{Mul})^{−1}.

Русский

Для каждого x в Additive α образ отрицания под умножением равен обратному: (−x)^{Mul} = (x^{Mul})^{−1}.

LaTeX

$$(-x)^{Mul} = (x^{Mul})^{-1}$$

Lean4

@[simp]
theorem toMul_neg [Inv α] (x : Additive α) : (-x).toMul = x.toMul⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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