Theorems · Theorem · group theory

FreeAddGroupBasis.lift_apply_apply

∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (a : ι → H) (x : G), (b.lift a) x = (FreeAddGroup.lift a) (b.repr x)

Defined in

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddGroup