[Merged by Bors] - feat(LinearAlgebra/QuadraticForm/TensorProduct): base change of quadratic forms

[eric-wieser]

---

• depends on: [Merged by Bors] - feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms #6306

[eric-wieser]

I also tried to prove:

theorem _root_.BilinForm.toQuadraticForm_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) :
    (B₁.tmul B₂).toQuadraticForm
      = B₁.toQuadraticForm.tmul B₂.toQuadraticForm := by
  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
  rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul]
  dsimp
  refine (associated_rightInverse R).injective ?_
  refine BilinForm.toLin.injective ?_
  ext a₁ a₂ b₁ b₂
  dsimp [-associated_apply]
  simp [sub_smul, smul_sub, add_smul, smul_add, ←smul_mul_smul]
  set aa₁ := B₁ a₁ a₁
  set ab₁ := B₁ a₁ b₁
  set ba₁ := B₁ b₁ a₁
  set bb₁ := B₁ b₁ b₁
  set aa₂ := B₂ a₂ a₂
  set ab₂ := B₂ a₂ b₂
  set ba₂ := B₂ b₂ a₂
  set bb₂ := B₂ b₂ b₂
  sorry

though the algebra is too painful to get to a point where it's obvious whether it's true.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms #6306
  By Dependent Issues (🤖). Happy coding!

[alexjbest]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alexjbest.

[ocfnash]

Thanks!

bors d+

[bors]

✌️ eric-wieser 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]

bors merge

[bors]

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style