From ff0a3e96487036585cd829a28633b2504f598d30 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 19:55:11 +0800 Subject: [PATCH] chore(LinearAlgebra/CliffordAlgebra/SpinGroup): remove an erw --- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean index 7a89455eb57e99..9917233aedbacd 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean @@ -136,7 +136,7 @@ theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzG refine Eq.trans_le ?_ this simp only [map_inv, smul_inv_smul] intro x hx - erw [Submodule.map_le_iff_le_comap] + rw [Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap] rintro _ ⟨m, rfl⟩ exact conjAct_smul_ι_mem_range_ι hx _