Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f g : SkewMonoidAlgebra k G) (x : G) (s : Finset (G × G)),
  (∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) → (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMulSMulZeroClass