renaming

leanprover-community · Sep 15, 2024 · 6092636 · 6092636
1 parent 9cffe27
commit 6092636
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean
@@ -173,7 +173,7 @@ theorem eq_const_of_zero {n : SimplexCategory} (f : ([0] : SimplexCategory) ⟶
     f = const _ n (f.toOrderHom 0) := by
   ext x; match x with | 0 => rfl
 
-theorem eq_const_of_zero' {n : SimplexCategory} (f : ([0] : SimplexCategory) ⟶ n) :
+theorem exists_eq_const_of_zero {n : SimplexCategory} (f : ([0] : SimplexCategory) ⟶ n) :
     ∃ a, f = const _ n a := ⟨_, eq_const_of_zero _⟩
 
 theorem eq_const_to_zero {n : SimplexCategory} (f : n ⟶ [0]) :