# Zulip Chat Archive

## 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,
nat.cast_one, matrix.cons_add_cons, matrix.cons_eq_zero_iff,
eq_iff_true_of_subsingleton, and_true], -- found with `squeeze_simp [fin.sum_univ_succ]`
norm_num },
{ use 0, norm_num }
end
```

#### Eric Rodriguez (Jul 25 2022 at 00:16):

Adam, if you add the import `import algebra.big_operators.norm_num`

then `norm_num`

does all of the first case :)

Last updated: Dec 20 2023 at 11:08 UTC