Theorems · Theorem · commutative algebra

AddMonoidAlgebra.divOf_add

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G) (a b : G), x.divOf (a + b) = (x.divOf a).divOf b

Defined in

Mathlib.Algebra.MonoidAlgebra.Division

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidIsCancelAdd