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 aesopis an overkill for this.


Last updated: May 02 2025 at 03:31 UTC