feat: port Mathlib.Data.List.Range (#1463)

leanprover-community · Jan 10, 2023 · cbea84f · cbea84f
1 parent daa535f
commit cbea84f
Show file tree

Hide file tree

Showing 2 changed files with 330 additions and 38 deletions.
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
@@ -44,6 +44,6 @@ end Finset
 namespace Fintype
 
 instance (n : ℕ) : Fintype (Fin n) :=
-  ⟨⟨List.finRange n, List.nodup_fin_range n⟩, List.mem_fin_range⟩
+  ⟨⟨List.finRange n, List.nodup_finRange n⟩, List.mem_finRange⟩
 
 end Fintype