isRelPrime_self

Mathlib.Algebra.Divisibility.Units

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

English

IsRelPrime x x iff IsUnit x.

Русский

IsRelPrime x x эквивалентно IsUnit x.

LaTeX

$$$$\operatorname{IsRelPrime}(x,x) \iff \operatorname{IsUnit}(x).$$$$

Lean4

theorem isRelPrime_self : IsRelPrime x x ↔ IsUnit x :=
  ⟨(· dvd_rfl dvd_rfl), fun hu _ _ dvd ↦ isUnit_of_dvd_unit dvd hu⟩

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

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

Разделы

Аффилиация

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