toIdeal_mul

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.toIdeal_mul

English

The toIdeal map respects multiplication: (I · J).toIdeal = I.toIdeal · J.toIdeal.

Русский

Переменная toIdeal сохраняет произведение: (I · J).toIdeal = I.toIdeal · J.toIdeal.

LaTeX

$$$ (I \cdot J).toIdeal = I.toIdeal \cdot J.toIdeal $$$

Lean4

@[simp]
theorem toIdeal_mul (I J : HomogeneousIdeal 𝒜) : (I * J).toIdeal = I.toIdeal * J.toIdeal :=
  rfl

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

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

Разделы

Аффилиация

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