Theorems · Theorem · group theory

vadd_zero_vadd

∀ {α : Type u_5} {M : Type u_9} (N : Type u_10) [inst : AddMonoid N] [inst_1 : VAdd M N] [inst_2 : AddAction N α]
  [inst_3 : VAdd M α] [VAddAssocClass M N α] (x : M) (y : α), (x +ᵥ 0) +ᵥ y = x +ᵥ y

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

8 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

AddMonoidVAddAddActionVAddVAddAssocClass