isRelPrime_zero_right

Mathlib.Algebra.GroupWithZero.Divisibility

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

English

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

Русский

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

LaTeX

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

Lean4

theorem isRelPrime_zero_right : IsRelPrime x 0 ↔ IsUnit x :=
  isRelPrime_comm.trans isRelPrime_zero_left

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

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

Разделы

Аффилиация

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