α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ get k (map (fun a => -a) as) = -get k as
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ get k (neg as) = -get k as
unfold neg
case a
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ -default = default
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ get k (map (fun a => -a) as) = -get k as
rw [@get_map' α α ⟨0⟩ ⟨0⟩]
no goals
case a
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ -default = default
apply neg_zero