instNontrivialOfNonempty

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

If k is nontrivial and G is nonempty, then SkewMonoidAlgebra k G is nontrivial; for instance, ⟨0⟩ ≠ ⟨1⟩.

Русский

Если k ненулевой и G непуст, то SkewMonoidAlgebra k G ненулевой; например, ⟨0⟩ ≠ ⟨1⟩.

LaTeX

$$$ \langle 0 \rangle \neq \langle 1 \rangle $$$

Lean4

instance [Nontrivial k] [Nonempty G] : Nontrivial (SkewMonoidAlgebra k G) :=
  Function.Injective.nontrivial ofFinsupp_injective

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

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

Разделы

Аффилиация

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