instRing

Mathlib.Algebra.Ring.CentroidHom

URI: https://scilib.ai/kg/mathlib#CentroidHom.instRing

← MathLib Explorer

English

The ring structure on CentroidHom α is established via toEnd and natCast.

Русский

Кольцевую структуру на CentroidHom α задают через toEnd и natCast.

LaTeX

$$$Ring(\mathrm{CentroidHom}(\alpha))$$$

Lean4

instance instRing : Ring (CentroidHom α) :=
  toEnd_injective.ring _ toEnd_zero toEnd_one toEnd_add toEnd_mul toEnd_neg toEnd_sub toEnd_smul toEnd_smul toEnd_pow
    toEnd_natCast toEnd_intCast

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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