[Merged by Bors] - feat(data/matrix/basic): add missing smul instances, generalize lemmas to work on scalar towers#7544
Conversation
…s to work on scalar towers This also fixes the `add_monoid_hom.map_zero` etc lemmas to not require overly strong typeclasses on `α`
| section homs | ||
|
|
||
| -- TODO: there should be a way to avoid restating these for each `foo_hom`. | ||
| /-- A version of `one_map` where `f` is a ring hom. -/ | ||
| @[simp] lemma ring_hom_map_one [decidable_eq n] | ||
| {β : Type w} [semiring β] (f : α →+* β) : | ||
| @[simp] lemma ring_hom_map_one [decidable_eq n] [semiring α] [semiring β] (f : α →+* β) : | ||
| (1 : matrix n n α).map f = 1 := | ||
| one_map f.map_zero f.map_one |
There was a problem hiding this comment.
These were previously in a section with [semiring α], which was wrong for most of the lemmas
| /- This line does not type-check without `id` and `: _`. Lean did not recognize that two different | ||
| `add_monoid` instances were def-eq -/ |
There was a problem hiding this comment.
I figured since this showed up in the diff I may as well sort it out - the problem this refers to doesn't seem to happen any more.
| (L ⬝ M).map f = L.map f ⬝ M.map f := | ||
| by { ext, simp [mul_apply, ring_hom.map_sum], } | ||
|
|
||
| lemma is_add_monoid_hom_mul_left (M : matrix l m α) : |
There was a problem hiding this comment.
Do we want bundled versions of these?
There was a problem hiding this comment.
Maybe, but I'd argue that's out of scope - these lines are just moved from below
There was a problem hiding this comment.
I can split the PR to make this move clearer if you like?
|
|
||
| section star_ring | ||
| variables [decidable_eq n] {R : Type*} [semiring R] [star_ring R] | ||
| variables [decidable_eq n] [semiring α] [star_ring α] |
There was a problem hiding this comment.
Hmm, now you are moving from "meaningful variable name" to "generic type variable name". Why?
There was a problem hiding this comment.
Because this is the only section of this file to use R for the coefficients of the matrix.
There was a problem hiding this comment.
I think we should rather change the rest of the file. But in another PR.
There was a problem hiding this comment.
I agree, although I'm not sure what letter I would use for the scalar action type if R were reserved for the coefficients.
There was a problem hiding this comment.
In that spot, I would use S for the coefficients, or A.
…s to work on scalar towers (#7544) This also fixes the `add_monoid_hom.map_zero` etc lemmas to not require overly strong typeclasses on `α` This removes the `matrix.smul_apply` lemma since `pi.smul_apply` and `smul_eq_mul` together replace it.
|
Pull request successfully merged into master. Build succeeded: |
This also fixes the
add_monoid_hom.map_zeroetc lemmas to not require overly strong typeclasses onαThis removes the
matrix.smul_applylemma sincepi.smul_applyandsmul_eq_multogether replace it.