isUnit_of_dvd

Mathlib.RingTheory.Coprime.Basic

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

← MathLib Explorer

English

If IsCoprime x y and x divides y, then x is a unit.

Русский

Если IsCoprime x y и x делится на y, то x является единицей.

LaTeX

$$$IsCoprime(x,y) \land x \mid y \Rightarrow IsUnit(x)$$$

Lean4

theorem isUnit_of_dvd (H : IsCoprime x y) (d : x ∣ y) : IsUnit x :=
  let ⟨k, hk⟩ := d
  isCoprime_self.1 <| IsCoprime.of_mul_right_left <| show IsCoprime x (x * k) from hk ▸ H

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

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

Разделы

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

Аффилиация

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