instRingEquivClass

Mathlib.Algebra.Star.StarRingHom

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

English

The collection of star ring equivalences from A to B forms a RingEquivClass between A and B.

Русский

Множество звёздно-кольцевых эквивалентностей между A и B образует RingEquivClass между A и B.

LaTeX

$$$\\text{RingEquivClass}(A \\simeq_{\\star} B)$$$

Lean4

instance : RingEquivClass (A ≃⋆+* B) A B where
  map_mul f := f.map_mul'
  map_add f := f.map_add'

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

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

Разделы

Аффилиация

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