[Merged by Bors] - chore(data/matrix/notation): split into 2 files

[urkud]

I want to use ![a, b] notation in some files that don't need to import data.matrix.basic.

---

[eric-wieser]

Can you look through the other 13 files that import this and see if they can be relaxed too?

[eric-wieser]

bors d+

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

CI is failing because these two lemmas need to move to the fin file:

mathlib/src/data/matrix/notation.lean

Line 210 in e714e39

@[simp] lemma smul_empty (x : α) (v : fin 0 → α) : x • v = ![] := empty_eq _

mathlib/src/data/matrix/notation.lean

Lines 214 to 216 in e714e39

	@[simp] lemma smul_cons (x y : α) (v : fin n → α) :
	x • vec_cons y v = vec_cons (x * y) (x • v) :=
	by { ext i, refine fin.cases _ _ i; simp }

[eric-wieser]

This example is weird, because lean doesn't even know this has type matrix so doesn't use this instance. Out of scope I guess though, since it was here before.

[urkud]

CI is failing because these two lemmas need to move to the fin file:

Then it will have to import algebra.module.pi

[eric-wieser]

I think that's fine. If it becomes a problem in future, then I'd argue the solution is to split a group_theory.group_action.pi module out of algebra.module.pi, to match group_theory.group_action.prod.

[eric-wieser]

bors d+

The CI failure is weird

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests