neg

Mathlib.Algebra.Ring.Units

URI: https://scilib.ai/kg/mathlib#IsUnit.neg

English

If a is a unit, then −a is also a unit (in a ring with distributing negation).

Русский

Если a является элементом-единицей, то и −a также является единицей.

LaTeX

$$IsUnit a → IsUnit (−a)$$

Lean4

theorem neg [Monoid α] [HasDistribNeg α] {a : α} : IsUnit a → IsUnit (-a)
  | ⟨x, hx⟩ => hx ▸ (-x).isUnit

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

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

Разделы

Аффилиация

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