isRelPrime_zero_left

Mathlib.Algebra.GroupWithZero.Divisibility

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

English

IsRelPrime 0 x is equivalent to IsUnit x in a commutative monoid with zero.

Русский

IsRelPrime 0 x эквивалентно IsUnit x в коммутативной моноиде с нулём.

LaTeX

$$IsRelPrime(0, x) \iff IsUnit(x)$$

Lean4

theorem isRelPrime_zero_left : IsRelPrime 0 x ↔ IsUnit x :=
  ⟨(· (dvd_zero _) dvd_rfl), IsUnit.isRelPrime_right⟩

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

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

Разделы

Аффилиация

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