map_mul

Mathlib.Algebra.Ring.Equiv

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

English

A ring isomorphism preserves multiplication: for all x,y in R, e(xy) = e(x)e(y).

Русский

Кольцевой изоморфизм сохраняет умножение: для всех x,y ∈ R выполняется e(xy) = e(x)e(y).

LaTeX

$$$\\forall x,y \\in R,\\ e(xy) = e(x)\\,e(y)$$$

Lean4

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

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

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

Разделы

Аффилиация

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