coe_sub

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.coe_sub

← MathLib Explorer

English

Coercion commutes with scalar multiplication from R'.

Русский

Коэрцирование commute с умножением на скаляр из R'.

LaTeX

$$coe_smul : ↑(r • x) = r • (x : A)$$

Lean4

protected theorem coe_sub {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [Star A]
    {S : NonUnitalStarSubalgebra R A} (x y : S) : (↑(x - y) : A) = ↑x - ↑y :=
  rfl

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

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

Разделы

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

Аффилиация

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