[Merged by Bors] - feat(LinearAlgebra/QuadraticForm/Basic): more lemmas#7196
[Merged by Bors] - feat(LinearAlgebra/QuadraticForm/Basic): more lemmas#7196eric-wieser wants to merge 4 commits intomasterfrom
Conversation
| rfl | ||
| #align quadratic_form.associated_apply QuadraticForm.associated_apply | ||
|
|
||
| theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by |
There was a problem hiding this comment.
| theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by | |
| @[simp] theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by |
| polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by | ||
| rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul, | ||
| ←LinearMap.map_smul, smul_tmul', ←two_nsmul_associated R] | ||
| erw [associated_sq] |
There was a problem hiding this comment.
How about adding something like:
lemma associatedHom_apply {R M S : Type*} [CommRing R]
[AddCommGroup M] [Module R M] [CommRing S] [Algebra S R] [Invertible (2 : R)]
(Q : QuadraticForm R M) :
associatedHom S Q = associated Q := by
rfljust below the definition of associated and using it to avoid the erw (so that this whole proof just becomes one giant chain of rws).
There was a problem hiding this comment.
This associatedHom thing is a mess that I was considering cleaning up another time. I think the canonical spelling should be an unbundled one, with the hom available if needed.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
This also adds a handful of missing lemmas about `Set.center` for inverses and numeric literals.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This also adds a handful of missing lemmas about `Set.center` for inverses and numeric literals.
This also adds a handful of missing lemmas about
Set.centerfor inverses and numeric literals.