lsingle_apply — Mathlib

English

The value of the lsingle map on an element b of k equals the coefficient at a in the corresponding basis element, i.e., lsingle a b = single a b.

Русский

Значение отображения lsingle на элемент b равняется коэффициенту при базисном элементе a, т.е. lsingle a b = single a b.

LaTeX

$$$$lsingle \ (R := R)\ a \ b = single\ a\ b,$$$$

Lean4

@[simp]
theorem lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) : lsingle (R := R) a b = single a b :=
  rfl

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