Theorems · Theorem · group theory

Abelianization.lift_unique

∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A] (f : G →* A) (φ : Abelianization G →* A),
  (∀ (x : G), φ (Abelianization.of x) = f x) → ∀ {x : Abelianization G}, φ x = (Abelianization.lift f) x

Defined in

Mathlib.GroupTheory.Abelianization.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupCommGroup