mono

Mathlib.RingTheory.Coprime.Basic

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

← MathLib Explorer

English

If x|y and z|w and IsCoprime(y,w), then IsCoprime(x,z).

Русский

Если x делится на y и z делится на w и IsCoprime(y,w), тогда IsCoprime(x,z).

LaTeX

$$$x \mid y \land z \mid w \land IsCoprime(y,w) \Rightarrow IsCoprime(x,z)$$$

Lean4

@[gcongr]
theorem mono (h₁ : x ∣ y) (h₂ : z ∣ w) (h : IsCoprime y w) : IsCoprime x z :=
  h.of_isCoprime_of_dvd_left h₁ |>.of_isCoprime_of_dvd_right h₂

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

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

Разделы

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

Аффилиация

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