instStarRingEquivClass

Mathlib.Algebra.Star.StarRingHom

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

English

The collection StarRingEquiv A B is equipped with a structure that makes it a StarRingEquivClass between A and B.

Русский

Сборка StarRingEquiv A B наделяет StarRingEquivClass между A и B.

LaTeX

$$$\\text{StarRingEquiv} \\; A \\; B \\text{ является }\\; \\text{StarRingEquivClass}(A,B)$$$

Lean4

instance : StarRingEquivClass (A ≃⋆+* B) A B where map_star := map_star'

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

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

Разделы

Аффилиация

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