mul_sup_eq_of_coprime_left

Mathlib.RingTheory.Ideal.Operations

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

← MathLib Explorer

English

If I ⊔ J = ⊤, then I ⊔ J K = K ⊔ J.

Русский

Если I ⊔ J = ⊤, то I ⊔ J K = K ⊔ J.

LaTeX

$$$ I \oplus J K = K \oplus J \quad \text{when } I \oplus J = 1. $$$

Lean4

theorem mul_sup_eq_of_coprime_left (h : I ⊔ J = ⊤) : I * K ⊔ J = K ⊔ J :=
  by
  rw [sup_comm] at h
  rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

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

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

Разделы

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

Аффилиация

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