one_dvd

Mathlib.Algebra.Divisibility.Basic

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

English

1 divides any element a.

Русский

1 делит любое a.

LaTeX

$$$$1 \mid a.$$$$

Lean4

theorem one_dvd (a : α) : 1 ∣ a :=
  Dvd.intro a (one_mul a)

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

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

Разделы

Аффилиация

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