α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.comp (map g) (map f)) x = ↑(map g) (↑(map f) x)
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(map (g ∘ f)) x = ↑(map g) (↑(map f) x)
rw [map_comp]
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.comp (map g) (map f)) x = ↑(map g) (↑(map f) x)
rfl