[Merged by Bors] - refactor(Data/Matrix/Basic): use a defeq for scalar that matches its docstring #8115
Conversation
…ast` This also gives the `intCast` instance a nicer defeq. This remains unopinionated about which side of `diagonal 37 = 37` is the simp-normal form.
eric-wieser
added
blocked-by-other-PR
eric-wieser
changed the title
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
| #noalign matrix.scalar_apply_eq | ||
| #noalign matrix.scalar_apply_ne |
There was a problem hiding this comment.
I would prefer to keep these two specialized apply lemmas (they don't need to be @[simp]), it seems to save a bit of work down the line. Also because many of the specializations of diagonal also have this apply_eq and apply_ne variation.
There was a problem hiding this comment.
Also because many of the specializations of
diagonalalso have thisapply_eqandapply_nevariation.
What lemmas are you thinking of?
There was a problem hiding this comment.
A quick search for apply_(of_)?ne gives the following @[simp] lemmas about on/off diagonal entries of matrices: one_apply_{eq,ne}, charmatrix_apply_{eq,ne}, stdBasisMatrix.apply_{same,of_ne}, stdBasisMatrix.mul_{left,right}_apply_of_ne, transvection_mul_apply_of_ne.
More generally, we have AffineBasis.coord_apply_{eq,ne}, CategoryTheory.Mat.id_apply_of_ne, Finset.affineCombinationSingleWeights_apply_of_ne, Finset.weightedVSubVSubWeights_apply_of_ne, Finset.affineCombinationLineMapWeights_apply_of_ne, Finsupp.single_eq_of_ne.
I haven't counted but these apply lemmas are more commonly marked as @[simp] than not.
There was a problem hiding this comment.
I'd argue it's better to just force the user to unfold scalar (using scalar_apply) if they want any lemmas about it; its primary purpose is to exist as a bundled morphism. The alternative feels like a path to duplicating all the diagonal API for scalar, which seems like a lot of work to save using a dsimp lemma.
There was a problem hiding this comment.
Alright! I haven't been entirely convinced but it's not worth holding up this PR on that.
Vierkantor
added
awaiting-author
eric-wieser
added
awaiting-review
| #noalign matrix.scalar_apply_eq | ||
| #noalign matrix.scalar_apply_ne |
There was a problem hiding this comment.
A quick search for apply_(of_)?ne gives the following @[simp] lemmas about on/off diagonal entries of matrices: one_apply_{eq,ne}, charmatrix_apply_{eq,ne}, stdBasisMatrix.apply_{same,of_ne}, stdBasisMatrix.mul_{left,right}_apply_of_ne, transvection_mul_apply_of_ne.
More generally, we have AffineBasis.coord_apply_{eq,ne}, CategoryTheory.Mat.id_apply_of_ne, Finset.affineCombinationSingleWeights_apply_of_ne, Finset.weightedVSubVSubWeights_apply_of_ne, Finset.affineCombinationLineMapWeights_apply_of_ne, Finsupp.single_eq_of_ne.
I haven't counted but these apply lemmas are more commonly marked as @[simp] than not.
|
bors merge |
github-actions
bot
removed
the
awaiting-review
…docstring (#8115) This changes the defeq from `scalar a = a • 1` to `scalar a = diagonal fun _ => a`, which has the nice bonus of making `algebraMap_eq_diagonal` true by `rfl`. As a result, we need a new `smul_one_eq_diagonal` lemma to rewrite `diagonal fun _ => a` back into `a • 1`, along with some variants for convenience. In the long term we could generalize this to non-unital rings, now that it needs no `1`.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…docstring (#8115) This changes the defeq from `scalar a = a • 1` to `scalar a = diagonal fun _ => a`, which has the nice bonus of making `algebraMap_eq_diagonal` true by `rfl`. As a result, we need a new `smul_one_eq_diagonal` lemma to rewrite `diagonal fun _ => a` back into `a • 1`, along with some variants for convenience. In the long term we could generalize this to non-unital rings, now that it needs no `1`.
This changes the defeq from
scalar a = a • 1toscalar a = diagonal fun _ => a, which has the nice bonus of makingalgebraMap_eq_diagonaltrue byrfl.As a result, we need a new
smul_one_eq_diagonallemma to rewritediagonal fun _ => aback intoa • 1, along with some variants for convenience.In the long term we could generalize this to non-unital rings, now that it needs no
1.natCastandintCast#8088