map_add

Mathlib.RingTheory.FractionalIdeal.Operations

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

English

The map distributes over addition: map g (I + J) = map g I + map g J.

Русский

Образ отображения через g распределяется по сложению: map g (I + J) = map g I + map g J.

LaTeX

$$$ (I + J).map g = I.map g + J.map g $$$

Lean4

@[simp]
protected theorem map_add : (I + J).map g = I.map g + J.map g :=
  coeToSubmodule_injective (Submodule.map_sup _ _ _)

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

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

Разделы

Аффилиация

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