coeff_one_one

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

The coefficient of 1 at 1 is 1: coeff(1) 1 = 1.

Русский

Коэффициент единицы по индексу 1 равен 1: coeff(1) 1 = 1.

LaTeX

$$$\\operatorname{coeff}(1)\\, 1 = 1$$$

Lean4

@[simp]
theorem coeff_one_one : coeff (1 : SkewMonoidAlgebra k G) 1 = 1 := by
  simp only [coeff, toFinsupp_single, Finsupp.single_eq_same]

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

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

Разделы

Аффилиация

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