mul

Mathlib.Data.PNat.Prime

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ m.Coprime k \\rightarrow n.Coprime k \\rightarrow (m \\cdot n).Coprime k $$$

Lean4

theorem mul {k m n : ℕ+} : m.Coprime k → n.Coprime k → (m * n).Coprime k :=
  by
  repeat rw [← coprime_coe]
  rw [mul_coe]
  apply Nat.Coprime.mul_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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