α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.id (FreeAbelianGroup α)) x = x
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup α
⊢ ↑(map id) x = x
rw [map_id]
no goals
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.id (FreeAbelianGroup α)) x = x
rfl