Theorems · Theorem · group theory

VAdd.comp.vaddCommClass

∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd β α]
  [VAddCommClass M β α] (g : N → M), VAddCommClass N β α

This cannot be an instance because it can cause infinite loops whenever the VAdd arguments are still metavariables.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

VAddVAddVAddCommClass