refactor(LinearAlgebra/BilinearMap): Congruences and bilinear maps

[mans0954]

Currently Mathlib has BilinForm.congr which defines a congruence between bilinear forms on the domain and range of an equivalence. This PR generalises this result to bilinear maps. The bilinear form version is recovered as a special case of the more general result.

Required for #8256

---

[j-loreaux]

I'm not convinced we need this at all, as it's just two applications of LinearEquiv.arrowCongr. And even if we did want it, it should take a third equivalence as an argument and be called LinearEquiv.arrowCongr₂

Suggested change

	/-- Apply linear equivalences on the arguments of a bilinear map. -/
	def congrl₁₂ (e₁ : Mₗ ≃ₗ[R] Nₗ) (e₂ : Pₗ ≃ₗ[R] Qₗ) :
	(Mₗ →ₗ[R] Pₗ →ₗ[R] M) ≃ₗ[R] (Nₗ →ₗ[R] Qₗ →ₗ[R] M) where
	/-- Apply linear equivalences on the arguments of a bilinear map. -/
	def congrl₁₂ (e₁ : Mₗ ≃ₗ[R] Nₗ) (e₂ : Pₗ ≃ₗ[R] Qₗ) :
	(Mₗ →ₗ[R] Pₗ →ₗ[R] M) ≃ₗ[R] (Nₗ →ₗ[R] Qₗ →ₗ[R] M) :=
	e₁.arrowCongr <| e₂.arrowCongr <| .refl R M

(Note this is definitionally equal to what you wrote.) If you want, you can update the definition of BilinForm.congr to use LinearEquiv.arrowCongr

[mans0954]

Not needed.