symm

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.Coprime.symm

English

If m and n are coprime, then n and m are coprime.

Русский

Если m и n взаимно простые, то n и m взаимно простые.

LaTeX

$$$ \text{Coprime}(m,n) \Rightarrow \text{Coprime}(n,m) $$$

Lean4

@[symm]
theorem symm {m n : ℕ+} : m.Coprime n → n.Coprime m :=
  by
  unfold Coprime
  rw [gcd_comm]
  simp

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

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

Разделы

Аффилиация

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