## Stream: new members

### Topic: simplifying matrix math

#### David Chanin (Jul 24 2022 at 20:58):

I'm trying to do a simple proof that says that there exists a number t such that [3,1,4], [2,-3,5], [5,9,t] is not linearly independent in R3. I'm framing the problem as below:

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
use [14, -3, 22, 7],
simp,
linarith,
end


basically, I just want it to subsitute these numbers into t, a, b, c and show that the results are equal. simp sort of helps, it does the smul and addition, but doesn't resolve the proof and leaves stuff in this weird form:

![-(3 * 3) + 22 * 2, -3 + -(22 * 3), -(3 * 4) + 22 * 5] = ![7 * 5, 7 * 9, 7 * 14]


Then, linarith throws an error. How can I get this to properly simplify and close the goal? It's just basic algebra to show these are the same thing

#### Eric Rodriguez (Jul 24 2022 at 20:59):

does ext x help?

#### Eric Rodriguez (Jul 24 2022 at 20:59):

after the use, before the simp

#### Eric Rodriguez (Jul 24 2022 at 20:59):

and maybe norm_num is the right thing

#### David Chanin (Jul 24 2022 at 21:01):

aah norm_num did it! Thanks so much!

#### Eric Wieser (Jul 24 2022 at 21:05):

congr' 1, {sorry}, congr' 1, { sorry } I think would let you equate each component separately, in case that's helpful

#### Eric Rodriguez (Jul 24 2022 at 21:07):

shouldn't we prefer interval_cases x?

#### David Chanin (Jul 24 2022 at 21:21):

ah doing congr' 1 { ... }3 times also works! That's handy to know

#### David Chanin (Jul 24 2022 at 21:21):

how would interval_cases work here?

#### David Chanin (Jul 24 2022 at 21:22):

( I also realized I had a mistake in the previous post, the correct values are as follows):

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
use [2, 3, -2 , 1],
simp,
norm_num,
end


#### Eric Rodriguez (Jul 24 2022 at 21:31):

sorry, I meant fin_cases!

#### Eric Rodriguez (Jul 24 2022 at 21:31):

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
use [2, 3, -2 , 1],
ext x,
fin_cases x,
/-
3 goals
⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 0 = (1 • ![5, 9, 2]) 0
⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 1 = (1 • ![5, 9, 2]) 1
⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 2 = (1 • ![5, 9, 2]) 2
-/
end


#### Patrick Johnson (Jul 24 2022 at 21:32):

Why not use all zeros? Or maybe the question is about tactics, rather than proving this exact statement?

example : ∃ (t a b c : ℝ), a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
⟨0, 0, 0, 0, by simp⟩


#### David Chanin (Jul 24 2022 at 21:34):

Ah that's a good point, I should add a constraint that a, b, and c can't be 0 too since that would also be a valid solution as I wrote it

#### Patrick Johnson (Jul 24 2022 at 21:38):

Alternatively, you could just drop c

example : ∃ (t a b : ℝ), a • ![3, 1, 4] + b • ![2, -3, 5] = ![5, 9, t] :=
⟨2, 3, -2, by norm_num⟩


#### David Chanin (Jul 24 2022 at 21:39):

Good call, that's even cleaner!

#### Eric Wieser (Jul 24 2022 at 22:07):

Are you aware of docs#linear_independent? Perhaps you already stated your problem that way and reduced it to the case above

#### David Chanin (Jul 24 2022 at 22:16):

That would probably be a smarter approach. I don't really understand how to use linear_independent though. How would I frame this problem in terms of using that term?

#### Eric Wieser (Jul 24 2022 at 22:38):

I think ∃ t : ℝ, ¬linear_independent ℝ ![![3, 1, 4], ![2, -3, 5], ![5, 9, t]] is the correct statement

#### David Chanin (Jul 24 2022 at 23:19):

ah ok, I'll see if I can figure out the proof that way, it does look a lot more legit

#### Eric Wieser (Jul 24 2022 at 23:21):

I imagine it will be more work to prove not less

#### Adam Topaz (Jul 25 2022 at 00:02):

If you simplify with docs#fin.sum_univ_succ that should reduce it easily to the previous proof

#### Adam Topaz (Jul 25 2022 at 00:06):

import data.real.basic
import linear_algebra.linear_independent

example : ∃ t : ℝ, ¬linear_independent ℝ ![![3, 1, 4], ![2, -3, 5], ![5, 9, t]] :=
begin
use 2,
rw [fintype.not_linear_independent_iff],
use ![3,-2,-1],
split,
{ simp only [fin.sum_univ_succ, matrix.cons_val_zero, matrix.smul_cons, algebra.id.smul_eq_mul,
mul_one, matrix.cons_val_succ, neg_mul, mul_neg, neg_neg, fintype.univ_of_subsingleton,
matrix.cons_val_fin_one, one_mul, finset.sum_const, finset.card_singleton, nsmul_eq_mul,
eq_iff_true_of_subsingleton, and_true], -- found with squeeze_simp [fin.sum_univ_succ]

Adam, if you add the import import algebra.big_operators.norm_num then norm_num does all of the first case :)