units_ne_iff_eq_neg

Mathlib.Algebra.Ring.Int.Units

URI: https://scilib.ai/kg/mathlib#Int.units_ne_iff_eq_neg

English

For units u,v ∈ ℤ^×, u ≠ v ↔ u = -v.

Русский

Для единиц u, v ∈ ℤ^×, соблюдается: u ≠ v ⇔ u = −v.

LaTeX

$$u \neq v \iff u = -v$$

Lean4

theorem units_ne_iff_eq_neg {u v : ℤˣ} : u ≠ v ↔ u = -v := by
  simpa only [Ne, Units.ext_iff] using isUnit_ne_iff_eq_neg u.isUnit v.isUnit

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

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

Разделы

Аффилиация

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