Theorems · Theorem · ring theory

SkewMonoidAlgebra.sum_congr

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {f : SkewMonoidAlgebra k G} {M : Type u_3}
  [inst_1 : AddCommMonoid M] {g₁ g₂ : G → k → M},
  (∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)) → f.sum g₁ = f.sum g₂

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid