instRingEquivClass

Mathlib.Algebra.Ring.Equiv

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

English

From a RingEquivClass F R S, construct an AddEquivClass on F respecting the additive structure.

Русский

Из RingEquivClass F R S строят AddEquivClass, совместимый с аддитивной структурой.

LaTeX

$$AddEquivClass F R S$$

Lean4

instance : RingEquivClass (R ≃+* S) R S where
  map_add f := f.map_add'
  map_mul f := f.map_mul'

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

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

Разделы

Аффилиация

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