map_add

Mathlib.Algebra.Ring.Equiv

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

English

A ring isomorphism preserves addition. For e : R ≃+* S and x,y ∈ R, e(x+y) = e x + e y.

Русский

Изоморфизм колец сохраняет сложение: для e : R ≃+* S и x,y ∈ R верно e(x+y) = e x + e y.

LaTeX

$$$e(x+y) = e x + e y$$$

Lean4

/-- A ring isomorphism preserves addition. -/
protected theorem map_add (e : R ≃+* S) (x y : R) : e (x + y) = e x + e y :=
  map_add e x y

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

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

Разделы

Аффилиация

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