Theorems · Theorem · ring theory

MonoidAlgebra.of_commute

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m : M} [inst_1 : MulOneClass M],
  (∀ (m' : M), Commute m m') → ∀ (f : MonoidAlgebra R M), Commute ((MonoidAlgebra.of R M) m) f

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMulOneClass