toFinsupp_eq_single_one_one_iff — Mathlib

English

With One G and AddMonoidWithOne k, an element a satisfies a.toFinsupp = single 1 1 if and only if a = 1.

Русский

Пусть есть единица G и AddMonoidWithOne k. Тогда a.toFinsupp = single 1 1 тогда и только если a = 1.

LaTeX

$$$a\\toFinsupp = Finsupp.single\\ 1\\ 1 \\iff a = 1$$$

Lean4

@[simp]
theorem toFinsupp_eq_single_one_one_iff {a : SkewMonoidAlgebra k G} : a.toFinsupp = Finsupp.single 1 1 ↔ a = 1 := by
  simp [← toFinsupp_inj]

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