doc: fix typo (#7067)

leanprover · Feb 13, 2025 · cc76c46 · cc76c46
1 parent b38da34
commit cc76c46
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
@@ -195,7 +195,7 @@ end Classical
 /- Export for Mathlib compat. -/
 export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
-/-- Extract an element from a existential statement, using `Classical.choose`. -/
+/-- Extract an element from an existential statement, using `Classical.choose`. -/
 -- This enables projection notation.
 @[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P