coeff_inj

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

The equality of coefficient functions implies equality of skew monoid algebra elements: p.coeff = q.coeff ⇔ p = q.

Русский

Равенство функций коэффициентов эквивалентно равенству элементов: p.coeff = q.coeff ⇔ p = q.

LaTeX

$$$ p.\mathrm{coeff} = q.\mathrm{coeff} \iff p = q $$$

Lean4

@[simp]
theorem coeff_inj (p q : SkewMonoidAlgebra k G) : p.coeff = q.coeff ↔ p = q :=
  coeff_injective.eq_iff

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

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

Разделы

Аффилиация

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