isUnit_of_dvd_one

Mathlib.Algebra.Divisibility.Units

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

English

If a divides 1, then a is a unit.

Русский

Если a делит 1, то a является единицей.

LaTeX

$$$$a \mid 1 \Rightarrow \operatorname{IsUnit}(a).$$$$

Lean4

theorem isUnit_of_dvd_one {a : α} (h : a ∣ 1) : IsUnit (a : α) :=
  isUnit_iff_dvd_one.mpr h

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

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

Разделы

Аффилиация

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