coeff_one

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.coeff_one

← MathLib Explorer

English

For any a, coeff(1) a = if a = 1 then 1 else 0.

Русский

Для любого a: coeff(1) a = 1, если a = 1, иначе 0.

LaTeX

$$$\\operatorname{coeff}(1)\\ a = \\begin{cases} 1, & a=1, \\\\ 0, & a \\neq 1. \\end{cases}$$$

Lean4

theorem coeff_one {a : G} [Decidable (a = 1)] : (1 : SkewMonoidAlgebra k G).coeff a = if a = 1 then 1 else 0 := by
  classical simpa [eq_comm (a := a)] using coeff_single_apply

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

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

Разделы

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

Аффилиация

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