Theorems · Theorem · group theory

add_vadd_comm

∀ {α : Type u_5} {β : Type u_6} [inst : Add β] [inst_1 : VAdd α β] [VAddCommClass α β β] (s : α) (x y : β),
  x + (s +ᵥ y) = s +ᵥ x + y

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

6 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

AddVAddVAddCommClass