isCoprime_iff_exists

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.isCoprime_iff_exists

English

IsCoprime I J iff ∃ i ∈ I, ∃ j ∈ J, i + j = 1.

Русский

IsCoprime I J эквивалентно существованию элементов i ∈ I и j ∈ J с i + j = 1.

LaTeX

$$$$ IsCoprime(I,J) \iff \exists i \in I, \exists j \in J, i + j = 1 $$$$

Lean4

theorem isCoprime_iff_exists : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by
  rw [← add_eq_one_iff, isCoprime_iff_add]

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

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

Разделы

Аффилиация

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