Update Mathlib/Data/Sign.lean

Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Jan 3, 2025 · 044e56e · 044e56e
1 parent cc712ea
commit 044e56e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Sign.lean b/Mathlib/Data/Sign.lean
@@ -434,7 +434,7 @@ theorem sign_pow (x : α) (n : ℕ) : sign (x ^ n) = sign x ^ n := map_pow signH
 lemma zero_mem_setRange_signTypeCast : (0 : α) ∈ Set.range SignType.cast :=
   ⟨0, rfl⟩
 
-lemma in_set_range_singType_cast_mul_in_set_range_singType_cast {a b : α}
+lemma mul_mem_setRange_signTypeCast {a b : α}
     (ha : a ∈ Set.range SignType.cast) (hb : b ∈ Set.range SignType.cast) :
     a * b ∈ Set.range SignType.cast := by
   obtain ⟨a', rfl⟩ := ha