Theorems · Theorem · group theory

Function.Surjective.vaddCommClass

∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAdd M β]
  [inst_3 : VAdd N β] [VAddCommClass M N α] {f : α → β},
  Function.Surjective f →
    (∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) → (∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) → VAddCommClass M N β

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

VAddVAddVAddVAddVAddCommClass