map_mul

Mathlib.RingTheory.FractionalIdeal.Operations

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.map_mul

← MathLib Explorer

English

The map preserves products: map g (I · J) = map g I · map g J.

Русский

Отображение сохраняет произведения: map g (I · J) = map g I · map g J.

LaTeX

$$$ (I \\cdot J).map g = I.map g \\cdot J.map g $$$

Lean4

@[simp]
protected theorem map_mul : (I * J).map g = I.map g * J.map g :=
  by
  simp only [mul_def]
  exact coeToSubmodule_injective (Submodule.map_mul _ _ _)

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

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

Разделы

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

Аффилиация

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