chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)

Adds dates to results deprecated in #12132 and #12078.

Mathlib/LinearAlgebra/BilinearForm/Hom.lean

@@ -60,18 +60,18 @@ def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R := A x
 #align bilin_form.to_lin_hom_aux₁ LinearMap.BilinForm.toLinHomAux₁
 
 /-- Auxiliary definition to define `toLinHom`; see below. -/
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R := A
 #align bilin_form.to_lin_hom_aux₂ LinearMap.BilinForm.toLinHomAux₂
 
 /-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in
 the right. -/
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := LinearMap.id
 #align bilin_form.to_lin_hom LinearMap.BilinForm.toLinHom
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem toLin'_apply (A : BilinForm R M) (x : M) : toLinHom (M := M) A x = A x :=
   rfl
 #align bilin_form.to_lin'_apply LinearMap.BilinForm.toLin'_apply
@@ -122,7 +122,7 @@ def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M := f
 
 set_option linter.deprecated false in
 /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R :=
   { BilinForm.toLinHom with
     invFun := LinearMap.toBilinAux
@@ -132,39 +132,39 @@ def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R]
 
 set_option linter.deprecated false in
 /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M :=
   BilinForm.toLin.symm
 #align linear_map.to_bilin LinearMap.toBilin
 
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem LinearMap.toBilinAux_eq (f : M →ₗ[R] M →ₗ[R] R) :
     LinearMap.toBilinAux f = f :=
   rfl
 #align linear_map.to_bilin_aux_eq LinearMap.toBilinAux_eq
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem LinearMap.toBilin_symm :
     (LinearMap.toBilin.symm : BilinForm R M ≃ₗ[R] _) = BilinForm.toLin :=
   rfl
 #align linear_map.to_bilin_symm LinearMap.toBilin_symm
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem BilinForm.toLin_symm :
     (BilinForm.toLin.symm : _ ≃ₗ[R] BilinForm R M) = LinearMap.toBilin :=
   LinearMap.toBilin.symm_symm
 #align bilin_form.to_lin_symm BilinForm.toLin_symm
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem LinearMap.toBilin_apply (f : M →ₗ[R] M →ₗ[R] R) (x y : M) :
     toBilin f x y = f x y :=
   rfl
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2024-04-26")]
 theorem BilinForm.toLin_apply (x : M) : BilinForm.toLin B x = B x :=
   rfl
 #align bilin_form.to_lin_apply BilinForm.toLin_apply