From bf8f75b3f6ac206385518dc03203477f1e7fa3e2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 20 Jun 2023 22:50:34 -0500
Subject: [PATCH] Use `nontrivial`

---
 src/analysis/convex/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index cb55d6488b422..91f5125b1aba7 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -563,7 +563,7 @@ end
 eq_univ_of_forall $ λ f, ⟨λ x, (subsingleton.elim _ _).le, subsingleton.elim _ _⟩
 
 /-- The standard simplex in the zero-dimensional space is empty. -/
-lemma std_simplex_of_empty [is_empty ι] [ne_zero (1 : 𝕜)] : std_simplex 𝕜 ι = ∅ :=
+lemma std_simplex_of_empty [is_empty ι] [nontrivial 𝕜] : std_simplex 𝕜 ι = ∅ :=
 eq_empty_of_forall_not_mem $ by { rintro f ⟨-, hf⟩, simpa using hf }
 
 lemma std_simplex_unique [unique ι] : std_simplex 𝕜 ι = {λ _, 1} :=