symmetric_isRelPrime

Mathlib.Algebra.Divisibility.Units

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

English

IsRelPrime is symmetric: IsRelPrime x y ⇔ IsRelPrime y x.

Русский

IsRelPrime симметрична: IsRelPrime x y ⇔ IsRelPrime y x.

LaTeX

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

Lean4

theorem symmetric_isRelPrime : Symmetric (IsRelPrime : α → α → Prop) := fun _ _ ↦ .symm

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

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

Разделы

Аффилиация

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