bump to nightly-2023-04-10-10

mathlib commit leanprover-community/mathlib@e05ead7
leanprover-community · Apr 10, 2023 · 5e0e4fa · 5e0e4fa
1 parent 8e02e5f
commit 5e0e4fa
Show file tree

Hide file tree

Showing 4 changed files with 508 additions and 22 deletions.
diff --git a/Mathbin/FieldTheory/Fixed.lean b/Mathbin/FieldTheory/Fixed.lean
@@ -284,7 +284,7 @@ theorem rank_le_card : Module.rank (FixedPoints.subfield G F) F ≤ Fintype.card
   rank_le fun s hs => by
     simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast,
       Cardinal.natCast_le] using
-      cardinal_lift_le_rank_of_linear_independent'
+      cardinal_lift_le_rank_of_linearIndependent'
         (linear_independent_smul_of_linear_independent G F hs)
 #align fixed_points.rank_le_card FixedPoints.rank_le_card