Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_single_apply

∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a a' : G} {b : k} [inst_1 : Decidable (a = a')],
  (SkewMonoidAlgebra.single a b).coeff a' = if a = a' then b else 0

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

2 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidDecidable