neg_iff

Mathlib.Algebra.Ring.Units

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

English

For a ring with distributive negation, IsUnit(−a) iff IsUnit(a).

Русский

Для кольца с распределённым отрицанием выполняется IsUnit(−a) ↔ IsUnit(a).

LaTeX

$$IsUnit(-a) ↔ IsUnit(a)$$

Lean4

@[simp]
theorem neg_iff [Monoid α] [HasDistribNeg α] (a : α) : IsUnit (-a) ↔ IsUnit a :=
  ⟨fun h => neg_neg a ▸ h.neg, IsUnit.neg⟩

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

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

Разделы

Аффилиация

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