codisjoint

Mathlib.RingTheory.Ideal.Operations

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

English

IsCoprime I J implies Codisjoint I J.

Русский

IsCoprime I J ⇒ Codisjoint I J.

LaTeX

$$$$ IsCoprime I J \Rightarrow Codisjoint I J $$$$

Lean4

theorem _root_.IsCoprime.codisjoint (h : IsCoprime I J) : Codisjoint I J :=
  isCoprime_iff_codisjoint.mp h

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

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

Разделы

Аффилиация

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