From f76443af1a32022341ca509a18e99690ff0426db Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 23 Apr 2026 23:16:15 +0800 Subject: [PATCH] chore: kill an in TensorProduct/Quotient --- Mathlib/LinearAlgebra/TensorProduct/Quotient.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index bc98cbfd4fae12..d0595a460fb70d 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -133,12 +133,7 @@ noncomputable def tensorQuotientEquiv (n : Submodule R N) : (M ⊗[R] N) ⧸ (LinearMap.range (map (LinearMap.id : M →ₗ[R] M) n.subtype)) := congr ((Submodule.quotEquivOfEqBot _ rfl).symm) (LinearEquiv.refl _ _) ≪≫ₗ quotientTensorQuotientEquiv (⊥ : Submodule R M) n ≪≫ₗ - Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by - simp only [Submodule.map_sup] - erw [Submodule.map_id, Submodule.map_id] - simp only [sup_eq_right] - rw [range_map_eq_span_tmul, range_map_eq_span_tmul] - simp) + Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by simp [range_map_eq_span_tmul]) @[simp] lemma tensorQuotientEquiv_apply_mk_tmul (n : Submodule R N) (x : M) (y : N) :