From 4935c5fcc123d1948ab4ff94e069c22922b8950d Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Tue, 16 Apr 2024 19:49:32 +0000 Subject: [PATCH] =?UTF-8?q?refactor(LinearAlgebra/BilinearForm/Basic):=20D?= =?UTF-8?q?erive=20the=20`*=5Fleft`=20and=20`*=5Fright`=20results=20from?= =?UTF-8?q?=20the=20`map=5F*=E2=82=82`=20and=20`map=5F*`=20results=20(#121?= =?UTF-8?q?24)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Following #11278 a number of the results in `LinearAlgebra/BilinearForm/Basic` are just special cases of results in `LinearAlgebra/BilinearMap`. --- Mathlib/LinearAlgebra/BilinearForm/Basic.lean | 30 +++++++------------ 1 file changed, 10 insertions(+), 20 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean index 7d8725a670002..812186c353ebd 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean @@ -69,12 +69,10 @@ theorem coeFn_congr : ∀ {x x' y y' : M}, x = x' → y = y' → B x y = B x' y' | _, _, _, _, rfl, rfl => rfl #align bilin_form.coe_fn_congr LinearMap.BilinForm.coeFn_congr -theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := by - simp only [map_add, LinearMap.add_apply] +theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := map_add₂ _ _ _ _ #align bilin_form.add_left LinearMap.BilinForm.add_left -theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := by - simp only [map_smul, LinearMap.smul_apply, smul_eq_mul] +theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := map_smul₂ _ _ _ _ #align bilin_form.smul_left LinearMap.BilinForm.smul_left theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := map_add _ _ _ @@ -83,28 +81,22 @@ theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := map_add _ _ _ theorem smul_right (a : R) (x y : M) : B x (a • y) = a * B x y := map_smul _ _ _ #align bilin_form.smul_right LinearMap.BilinForm.smul_right -theorem zero_left (x : M) : B 0 x = 0 := by - rw [← @zero_smul R _ _ _ _ (0 : M), smul_left, zero_mul] +theorem zero_left (x : M) : B 0 x = 0 := map_zero₂ _ _ #align bilin_form.zero_left LinearMap.BilinForm.zero_left -theorem zero_right (x : M) : B x 0 = 0 := by - rw [← @zero_smul R _ _ _ _ (0 : M), smul_right, zero_mul] +theorem zero_right (x : M) : B x 0 = 0 := map_zero _ #align bilin_form.zero_right LinearMap.BilinForm.zero_right -theorem neg_left (x y : M₁) : B₁ (-x) y = -B₁ x y := by - rw [← @neg_one_smul R₁ _ _, smul_left, neg_one_mul] +theorem neg_left (x y : M₁) : B₁ (-x) y = -B₁ x y := map_neg₂ _ _ _ #align bilin_form.neg_left LinearMap.BilinForm.neg_left -theorem neg_right (x y : M₁) : B₁ x (-y) = -B₁ x y := by - rw [← @neg_one_smul R₁ _ _, smul_right, neg_one_mul] +theorem neg_right (x y : M₁) : B₁ x (-y) = -B₁ x y := map_neg _ _ #align bilin_form.neg_right LinearMap.BilinForm.neg_right -theorem sub_left (x y z : M₁) : B₁ (x - y) z = B₁ x z - B₁ y z := by - rw [sub_eq_add_neg, sub_eq_add_neg, add_left, neg_left] +theorem sub_left (x y z : M₁) : B₁ (x - y) z = B₁ x z - B₁ y z := map_sub₂ _ _ _ _ #align bilin_form.sub_left LinearMap.BilinForm.sub_left -theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := by - rw [sub_eq_add_neg, sub_eq_add_neg, add_right, neg_right] +theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := map_sub _ _ _ #align bilin_form.sub_right LinearMap.BilinForm.sub_right lemma smul_left_of_tower (r : S) (x y : M) : B (r • x) y = r • B x y := by @@ -126,12 +118,10 @@ theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M theorem ext (H : ∀ x y : M, B x y = D x y) : B = D := ext₂ H #align bilin_form.ext LinearMap.BilinForm.ext -theorem congr_fun (h : B = D) (x y : M) : B x y = D x y := - h ▸ rfl +theorem congr_fun (h : B = D) (x y : M) : B x y = D x y := congr_fun₂ h _ _ #align bilin_form.congr_fun LinearMap.BilinForm.congr_fun -theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y := - ⟨congr_fun, ext₂⟩ +theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y := ext_iff₂ #align bilin_form.ext_iff LinearMap.BilinForm.ext_iff @[deprecated]