Zulip Chat Archive
Stream: new members
Topic: Why does this apply not work?
Abdullah Uyu (Mar 20 2024 at 16:26):
import Mathlib.LinearAlgebra.LinearIndependent
variable [DivisionRing K] [AddCommGroup V] [Module K V]
theorem lin_dep_aab (a b : V) : ¬ LinearIndependent K ![a, a, b] := by
intro aab_dep
rw [linearIndependent_iff'] at aab_dep
have aab_comb : (Finset.sum {0, 1, 2} fun i ↦ ![1, -1, 0] i • ![a, a, b] i) = 0 := by simp
apply (aab_dep {0, 1, 2} ![1, -1, 0]) at aab_comb
fails with
Failed to find (Finset.sum {0, 1, 2} fun i => ![1, -1, 0] i • ![a, a, b] i) =
0 as the type of a parameter of (Finset.sum {0, 1, 2} fun i => ![1, -1, 0] i • ![a, a, b] i) = 0 →
∀ i ∈ {0, 1, 2}, ![1, -1, 0] i = 0.
I am trying to eventually get an obvious contradiction here.
Abdullah Uyu (Mar 20 2024 at 17:01):
In other words, I want to instantiate aab_dep for {0,1,2}
and ![1,-1,0]
.
Abdullah Uyu (Mar 20 2024 at 17:06):
Oh, I am doing something silly.
Abdullah Uyu (Mar 20 2024 at 19:06):
Well, nevermind. I still don't understand what's going on here.
Abdullah Uyu (Mar 21 2024 at 07:18):
FWIW, the following works:
theorem lin_dep_aab (a b : V) : ¬ LinearIndependent K ![a, a, b] := by
intro aab_dep
rw [linearIndependent_iff'] at aab_dep
specialize aab_dep {0, 1, 2} ![1, -1, 0]
aesop
But, I suppose aesop
is an overkill for this.
Last updated: May 02 2025 at 03:31 UTC