Theorems · Theorem · group theory

FreeAbelianGroup.lift_unique

∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (f : α → β) (g : FreeAbelianGroup α →+ β),
  (∀ (x : α), g (FreeAbelianGroup.of x) = f x) → ∀ {x : FreeAbelianGroup α}, g x = (FreeAbelianGroup.lift f) x

Defined in

Mathlib.GroupTheory.FreeAbelianGroup

Cited by

3 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroup