inf_eq_mul_of_isCoprime

Mathlib.RingTheory.Ideal.Operations

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

English

If I and J are coprime, then I ∩ J = I·J.

Русский

Если I и J взаимно просты, то их пересечение равно произведению: I ∩ J = I·J.

LaTeX

$$$$ I \cap J = I J $$$$

Lean4

theorem inf_eq_mul_of_isCoprime (coprime : IsCoprime I J) : I ⊓ J = I * J :=
  (Ideal.mul_eq_inf_of_coprime coprime.sup_eq).symm

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

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

Разделы

Аффилиация

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