Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_single_mul_aux

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f : SkewMonoidAlgebra k G) {r : k} {x y z : G},
  (∀ (a : G), x * a = y ↔ a = z) → (SkewMonoidAlgebra.single x r * f).coeff y = r * x • f.coeff z

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringMulSMulZeroClass