Theorems · Theorem · group theory

AddSemiconjBy.vadd_right

∀ {M : Type u_1} {α : Type u_5} [inst : VAdd M α] [inst_1 : Add α] [VAddCommClass M α α] [VAddAssocClass M α α]
  {x a b : α}, AddSemiconjBy x a b → ∀ (r : M), AddSemiconjBy x (r +ᵥ a) (r +ᵥ b)

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

VAddAddVAddCommClassVAddAssocClass