isRelPrime

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.isRelPrime

English

If a and b are coprime, then a and b are related by a notion called IsRelPrime.

Русский

Если a и b взаимно просты, то они образуют отношение IsRelPrime.

LaTeX

$$$IsCoprime(a,b) \Rightarrow IsRelPrime(a,b)$$$

Lean4

theorem isRelPrime {a b : R} (h : IsCoprime a b) : IsRelPrime a b := fun _ ↦ h.isUnit_of_dvd'

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

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

Разделы

Аффилиация

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