mul_comm

Mathlib.RingTheory.Ideal.Operations

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

← MathLib Explorer

English

For ideals I and J in a commutative semiring, I · J = J · I.

Русский

Для идеалов I и J в коммутативном полугруппе выполняется I · J = J · I.

LaTeX

$$$ I \\cdot J = J \\cdot I $$$

Lean4

protected theorem mul_comm : I * J = J * I :=
  le_antisymm (mul_le.2 fun _ hrI _ hsJ => mul_mem_mul_rev hsJ hrI)
    (mul_le.2 fun _ hrJ _ hsI => mul_mem_mul_rev hsI hrJ)

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

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

Разделы

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

Аффилиация

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