isUnit_iff_forall_dvd

Mathlib.Algebra.Divisibility.Units

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

English

An element x is a unit iff x divides every element.

Русский

Элемент x является единицей тогда и только тогда, когда он делит любое элемент.

LaTeX

$$$$\operatorname{IsUnit}(x) \iff \forall y\, (x \mid y).$$$$

Lean4

theorem isUnit_iff_forall_dvd {x : α} : IsUnit x ↔ ∀ y, x ∣ y :=
  isUnit_iff_dvd_one.trans ⟨fun h _ => h.trans (one_dvd _), fun h => h _⟩

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

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

Разделы

Аффилиация

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