chore: camel cardinal_mk (#18808)

Rename `cardinal_mk` in lemma names to `cardinalMk` to follow the naming convention.

Author: YaelDillies

Mathlib/Algebra/AlgebraicCard.lean

@@ -29,16 +29,19 @@ theorem infinite_of_charZero (R A : Type*) [CommRing R] [IsDomain R] [Ring A] [A
     [CharZero A] : { x : A | IsAlgebraic R x }.Infinite :=
   infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat
 
-theorem aleph0_le_cardinal_mk_of_charZero (R A : Type*) [CommRing R] [IsDomain R] [Ring A]
+theorem aleph0_le_cardinalMk_of_charZero (R A : Type*) [CommRing R] [IsDomain R] [Ring A]
     [Algebra R A] [CharZero A] : ℵ₀ ≤ #{ x : A // IsAlgebraic R x } :=
   infinite_iff.1 (Set.infinite_coe_iff.2 <| infinite_of_charZero R A)
 
+@[deprecated (since := "2024-11-10")]
+alias aleph0_le_cardinal_mk_of_charZero := aleph0_le_cardinalMk_of_charZero
+
 section lift
 
 variable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A]
   [NoZeroSMulDivisors R A]
 
-theorem cardinal_mk_lift_le_mul :
+theorem cardinalMk_lift_le_mul :
     Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } ≤ Cardinal.lift.{v} #R[X] * ℵ₀ := by
   rw [← mk_uLift, ← mk_uLift]
   choose g hg₁ hg₂ using fun x : { x : A | IsAlgebraic R x } => x.coe_prop
@@ -49,30 +52,40 @@ theorem cardinal_mk_lift_le_mul :
   rintro x (rfl : g x = f)
   exact mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩
 
-theorem cardinal_mk_lift_le_max :
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_lift_le_mul := cardinalMk_lift_le_mul
+
+theorem cardinalMk_lift_le_max :
     Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } ≤ max (Cardinal.lift.{v} #R) ℵ₀ :=
-  (cardinal_mk_lift_le_mul R A).trans <|
-    (mul_le_mul_right' (lift_le.2 cardinal_mk_le_max) _).trans <| by simp
+  (cardinalMk_lift_le_mul R A).trans <|
+    (mul_le_mul_right' (lift_le.2 cardinalMk_le_max) _).trans <| by simp
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_lift_le_max := cardinalMk_lift_le_max
 
 @[simp]
-theorem cardinal_mk_lift_of_infinite [Infinite R] :
+theorem cardinalMk_lift_of_infinite [Infinite R] :
     Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } = Cardinal.lift.{v} #R :=
-  ((cardinal_mk_lift_le_max R A).trans_eq (max_eq_left <| aleph0_le_mk _)).antisymm <|
+  ((cardinalMk_lift_le_max R A).trans_eq (max_eq_left <| aleph0_le_mk _)).antisymm <|
     lift_mk_le'.2 ⟨⟨fun x => ⟨algebraMap R A x, isAlgebraic_algebraMap _⟩, fun _ _ h =>
       NoZeroSMulDivisors.algebraMap_injective R A (Subtype.ext_iff.1 h)⟩⟩
 
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_lift_of_infinite := cardinalMk_lift_of_infinite
+
 variable [Countable R]
 
 @[simp]
 protected theorem countable : Set.Countable { x : A | IsAlgebraic R x } := by
   rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]
-  apply (cardinal_mk_lift_le_max R A).trans
+  apply (cardinalMk_lift_le_max R A).trans
   simp
 
 @[simp]
-theorem cardinal_mk_of_countable_of_charZero [CharZero A] [IsDomain R] :
+theorem cardinalMk_of_countable_of_charZero [CharZero A] [IsDomain R] :
     #{ x : A // IsAlgebraic R x } = ℵ₀ :=
-  (Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinal_mk_of_charZero R A)
+  (Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinalMk_of_charZero R A)
+
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_of_countable_of_charZero := cardinalMk_of_countable_of_charZero
 
 end lift
 
@@ -81,18 +94,24 @@ section NonLift
 variable (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A]
   [NoZeroSMulDivisors R A]
 
-theorem cardinal_mk_le_mul : #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀ := by
+theorem cardinalMk_le_mul : #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀ := by
   rw [← lift_id #_, ← lift_id #R[X]]
-  exact cardinal_mk_lift_le_mul R A
+  exact cardinalMk_lift_le_mul R A
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_mul := cardinalMk_le_mul
 
 @[stacks 09GK]
-theorem cardinal_mk_le_max : #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀ := by
+theorem cardinalMk_le_max : #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀ := by
   rw [← lift_id #_, ← lift_id #R]
-  exact cardinal_mk_lift_le_max R A
+  exact cardinalMk_lift_le_max R A
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
 
 @[simp]
-theorem cardinal_mk_of_infinite [Infinite R] : #{ x : A // IsAlgebraic R x } = #R :=
-  lift_inj.1 <| cardinal_mk_lift_of_infinite R A
+theorem cardinalMk_of_infinite [Infinite R] : #{ x : A // IsAlgebraic R x } = #R :=
+  lift_inj.1 <| cardinalMk_lift_of_infinite R A
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_of_infinite := cardinalMk_of_infinite
 
 end NonLift
 

Mathlib/Algebra/MvPolynomial/Cardinal.lean

@@ -10,7 +10,7 @@ import Mathlib.SetTheory.Cardinal.Finsupp
 /-!
 # Cardinality of Multivariate Polynomial Ring
 
-The main result in this file is `MvPolynomial.cardinal_mk_le_max`, which says that
+The main result in this file is `MvPolynomial.cardinalMk_le_max`, which says that
 the cardinality of `MvPolynomial σ R` is bounded above by the maximum of `#R`, `#σ`
 and `ℵ₀`.
 -/
@@ -29,33 +29,41 @@ section TwoUniverses
 variable {σ : Type u} {R : Type v} [CommSemiring R]
 
 @[simp]
-theorem cardinal_mk_eq_max_lift [Nonempty σ] [Nontrivial R] :
+theorem cardinalMk_eq_max_lift [Nonempty σ] [Nontrivial R] :
     #(MvPolynomial σ R) = max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀ :=
   (mk_finsupp_lift_of_infinite _ R).trans <| by
     rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_max_lift := cardinalMk_eq_max_lift
+
 @[simp]
-theorem cardinal_mk_eq_lift [IsEmpty σ] : #(MvPolynomial σ R) = Cardinal.lift.{u} #R :=
+theorem cardinalMk_eq_lift [IsEmpty σ] : #(MvPolynomial σ R) = Cardinal.lift.{u} #R :=
   ((isEmptyRingEquiv R σ).toEquiv.trans Equiv.ulift.{u}.symm).cardinal_eq
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_lift := cardinalMk_eq_lift
+
 theorem cardinal_lift_mk_le_max {σ : Type u} {R : Type v} [CommSemiring R] : #(MvPolynomial σ R) ≤
     max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀ := by
   cases subsingleton_or_nontrivial R
   · exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
   cases isEmpty_or_nonempty σ
-  · exact cardinal_mk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
-  · exact cardinal_mk_eq_max_lift.le
+  · exact cardinalMk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
+  · exact cardinalMk_eq_max_lift.le
 
 end TwoUniverses
 
 variable {σ R : Type u} [CommSemiring R]
 
-theorem cardinal_mk_eq_max [Nonempty σ] [Nontrivial R] :
+theorem cardinalMk_eq_max [Nonempty σ] [Nontrivial R] :
     #(MvPolynomial σ R) = max (max #R #σ) ℵ₀ := by simp
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_max := cardinalMk_eq_max
+
 /-- The cardinality of the multivariate polynomial ring, `MvPolynomial σ R` is at most the maximum
 of `#R`, `#σ` and `ℵ₀` -/
-theorem cardinal_mk_le_max : #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀ :=
+theorem cardinalMk_le_max : #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀ :=
   cardinal_lift_mk_le_max.trans <| by rw [lift_id, lift_id]
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
+
 end MvPolynomial

Mathlib/Algebra/Polynomial/Cardinal.lean

@@ -23,14 +23,18 @@ open Cardinal
 namespace Polynomial
 
 @[simp]
-theorem cardinal_mk_eq_max {R : Type u} [Semiring R] [Nontrivial R] : #(R[X]) = max #R ℵ₀ :=
+theorem cardinalMk_eq_max {R : Type u} [Semiring R] [Nontrivial R] : #(R[X]) = max #R ℵ₀ :=
   (toFinsuppIso R).toEquiv.cardinal_eq.trans <| by
     rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
     rfl
 
-theorem cardinal_mk_le_max {R : Type u} [Semiring R] : #(R[X]) ≤ max #R ℵ₀ := by
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_max := cardinalMk_eq_max
+
+theorem cardinalMk_le_max {R : Type u} [Semiring R] : #(R[X]) ≤ max #R ℵ₀ := by
   cases subsingleton_or_nontrivial R
   · exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
-  · exact cardinal_mk_eq_max.le
+  · exact cardinalMk_eq_max.le
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
 
 end Polynomial

Mathlib/Data/W/Cardinal.lean

@@ -10,7 +10,7 @@ import Mathlib.SetTheory.Cardinal.Arithmetic
 # Cardinality of W-types
 
 This file proves some theorems about the cardinality of W-types. The main result is
-`cardinal_mk_le_max_aleph0_of_finite` which says that if for any `a : α`,
+`cardinalMk_le_max_aleph0_of_finite` which says that if for any `a : α`,
 `β a` is finite, then the cardinality of `WType β` is at most the maximum of the
 cardinality of `α` and `ℵ₀`.
 This can be used to prove theorems about the cardinality of algebraic constructions such as
@@ -34,12 +34,14 @@ namespace WType
 open Cardinal
 
 
-theorem cardinal_mk_eq_sum' : #(WType β) = sum (fun a : α => #(WType β) ^ lift.{u} #(β a)) :=
+theorem cardinalMk_eq_sum_lift : #(WType β) = sum fun a ↦ #(WType β) ^ lift.{u} #(β a) :=
   (mk_congr <| equivSigma β).trans <| by
     simp_rw [mk_sigma, mk_arrow]; rw [lift_id'.{v, u}, lift_umax.{v, u}]
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_sum' := cardinalMk_eq_sum_lift
+
 /-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
-theorem cardinal_mk_le_of_le' {κ : Cardinal.{max u v}}
+theorem cardinalMk_le_of_le' {κ : Cardinal.{max u v}}
     (hκ : (sum fun a : α => κ ^ lift.{u} #(β a)) ≤ κ) :
     #(WType β) ≤ κ := by
   induction' κ using Cardinal.inductionOn with γ
@@ -49,9 +51,11 @@ theorem cardinal_mk_le_of_le' {κ : Cardinal.{max u v}}
   cases' hκ with hκ
   exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_of_le' := cardinalMk_le_of_le'
+
 /-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
   is at most the maximum of the cardinality of `α` and `ℵ₀`  -/
-theorem cardinal_mk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
+theorem cardinalMk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
     #(WType β) ≤ max (lift.{v} #α) ℵ₀ :=
   (isEmpty_or_nonempty α).elim
     (by
@@ -60,7 +64,7 @@ theorem cardinal_mk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
       exact zero_le _)
     fun hn =>
     let m := max (lift.{v} #α) ℵ₀
-    cardinal_mk_le_of_le' <|
+    cardinalMk_le_of_le' <|
       calc
         (Cardinal.sum fun a => m ^ lift.{u} #(β a)) ≤ lift.{v} #α * ⨆ a, m ^ lift.{u} #(β a) :=
           Cardinal.sum_le_iSup_lift _
@@ -79,18 +83,28 @@ theorem cardinal_mk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
                     power_le_power_left
                       (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _))
 
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_le_max_aleph0_of_finite' := cardinalMk_le_max_aleph0_of_finite'
+
 variable {β : α → Type u}
 
-theorem cardinal_mk_eq_sum : #(WType β) = sum (fun a : α => #(WType β) ^ #(β a)) :=
-  cardinal_mk_eq_sum'.trans <| by simp_rw [lift_id]
+theorem cardinalMk_eq_sum : #(WType β) = sum (fun a : α => #(WType β) ^ #(β a)) :=
+  cardinalMk_eq_sum_lift.trans <| by simp_rw [lift_id]
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_eq_sum := cardinalMk_eq_sum
 
 /-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
-theorem cardinal_mk_le_of_le {κ : Cardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) :
-    #(WType β) ≤ κ := cardinal_mk_le_of_le' <| by simp_rw [lift_id]; exact hκ
+theorem cardinalMk_le_of_le {κ : Cardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) :
+    #(WType β) ≤ κ := cardinalMk_le_of_le' <| by simp_rw [lift_id]; exact hκ
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_of_le := cardinalMk_le_of_le
 
 /-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
   is at most the maximum of the cardinality of `α` and `ℵ₀`  -/
-theorem cardinal_mk_le_max_aleph0_of_finite [∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀ :=
-  cardinal_mk_le_max_aleph0_of_finite'.trans_eq <| by rw [lift_id]
+theorem cardinalMk_le_max_aleph0_of_finite [∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀ :=
+  cardinalMk_le_max_aleph0_of_finite'.trans_eq <| by rw [lift_id]
+
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_le_max_aleph0_of_finite := cardinalMk_le_max_aleph0_of_finite
 
 end WType

Mathlib/FieldTheory/Fixed.lean

@@ -296,10 +296,12 @@ theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [Co
       _)
   this.of_comp _
 
-theorem cardinal_mk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Field V] [Algebra K V]
+theorem cardinalMk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Field V] [Algebra K V]
     [FiniteDimensional K V] [Field W] [Algebra K W] :
     Cardinal.mk (V →ₐ[K] W) ≤ finrank W (V →ₗ[K] W) :=
-  (linearIndependent_toLinearMap K V W).cardinal_mk_le_finrank
+  (linearIndependent_toLinearMap K V W).cardinalMk_le_finrank
+
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_algHom := cardinalMk_algHom
 
 noncomputable instance AlgEquiv.fintype (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V]
     [FiniteDimensional K V] : Fintype (V ≃ₐ[K] V) :=

Mathlib/FieldTheory/IsAlgClosed/Classification.lean

@@ -36,7 +36,7 @@ namespace Algebra.IsAlgebraic
 variable (R L : Type u) [CommRing R] [CommRing L] [IsDomain L] [Algebra R L]
 variable [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L]
 
-theorem cardinal_mk_le_sigma_polynomial :
+theorem cardinalMk_le_sigma_polynomial :
     #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
   @mk_le_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
     (fun x : L =>
@@ -56,23 +56,28 @@ theorem cardinal_mk_le_sigma_polynomial :
       refine (Subtype.heq_iff_coe_eq ?_).1 h.2
       simp only [h.1, forall_true_iff]
 
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_le_sigma_polynomial := cardinalMk_le_sigma_polynomial
+
 /-- The cardinality of an algebraic extension is at most the maximum of the cardinality
 of the base ring or `ℵ₀`. -/
 @[stacks 09GK]
-theorem cardinal_mk_le_max : #L ≤ max #R ℵ₀ :=
+theorem cardinalMk_le_max : #L ≤ max #R ℵ₀ :=
   calc
     #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
-      cardinal_mk_le_sigma_polynomial R L
+      cardinalMk_le_sigma_polynomial R L
     _ = Cardinal.sum fun p : R[X] => #{x : L | x ∈ p.aroots L} := by
       rw [← mk_sigma]; rfl
     _ ≤ Cardinal.sum.{u, u} fun _ : R[X] => ℵ₀ :=
       (sum_le_sum _ _ fun _ => (Multiset.finite_toSet _).lt_aleph0.le)
     _ = #(R[X]) * ℵ₀ := sum_const' _ _
     _ ≤ max (max #(R[X]) ℵ₀) ℵ₀ := mul_le_max _ _
     _ ≤ max (max (max #R ℵ₀) ℵ₀) ℵ₀ :=
-      (max_le_max (max_le_max Polynomial.cardinal_mk_le_max le_rfl) le_rfl)
+      (max_le_max (max_le_max Polynomial.cardinalMk_le_max le_rfl) le_rfl)
     _ = max #R ℵ₀ := by simp only [max_assoc, max_comm ℵ₀, max_left_comm ℵ₀, max_self]
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
+
 end Algebra.IsAlgebraic
 
 end AlgebraicClosure
@@ -128,9 +133,9 @@ theorem cardinal_le_max_transcendence_basis (hv : IsTranscendenceBasis R v) :
   calc
     #K ≤ max #(Algebra.adjoin R (Set.range v)) ℵ₀ :=
       letI := isAlgClosure_of_transcendence_basis v hv
-      Algebra.IsAlgebraic.cardinal_mk_le_max _ _
+      Algebra.IsAlgebraic.cardinalMk_le_max _ _
     _ = max #(MvPolynomial ι R) ℵ₀ := by rw [Cardinal.eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩]
-    _ ≤ max (max (max #R #ι) ℵ₀) ℵ₀ := max_le_max MvPolynomial.cardinal_mk_le_max le_rfl
+    _ ≤ max (max (max #R #ι) ℵ₀) ℵ₀ := max_le_max MvPolynomial.cardinalMk_le_max le_rfl
     _ = _ := by simp [max_assoc]
 
 /-- If `K` is an uncountable algebraically closed field, then its

Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

@@ -234,7 +234,7 @@ theorem max_aleph0_card_le_rank_fun_nat : max ℵ₀ #K ≤ Module.rank K (ℕ 
   obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ℕ → K)
   let L := Subfield.closure (Set.range (fun i : ιK × ℕ ↦ bK i.1 i.2))
   have hLK : #L < #K := by
-    refine (Subfield.cardinal_mk_closure_le_max _).trans_lt
+    refine (Subfield.cardinalMk_closure_le_max _).trans_lt
       (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)
     rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
   letI := Module.compHom K (RingHom.op L.subtype)

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -158,15 +158,17 @@ end
 namespace LinearIndependent
 variable [StrongRankCondition R]
 
-theorem cardinal_mk_le_finrank [Module.Finite R M]
+theorem cardinalMk_le_finrank [Module.Finite R M]
     {ι : Type w} {b : ι → M} (h : LinearIndependent R b) : #ι ≤ finrank R M := by
   rw [← lift_le.{max v w}]
   simpa only [← finrank_eq_rank, lift_natCast, lift_le_nat_iff] using h.cardinal_lift_le_rank
 
+@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_finrank := cardinalMk_le_finrank
+
 theorem fintype_card_le_finrank [Module.Finite R M]
     {ι : Type*} [Fintype ι] {b : ι → M} (h : LinearIndependent R b) :
     Fintype.card ι ≤ finrank R M := by
-  simpa using h.cardinal_mk_le_finrank
+  simpa using h.cardinalMk_le_finrank
 
 theorem finset_card_le_finrank [Module.Finite R M]
     {b : Finset M} (h : LinearIndependent R (fun x => x : b → M)) :

Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

@@ -214,7 +214,7 @@ theorem Module.finrank_le_one_iff_top_isPrincipal [Module.Free K V] [Module.Fini
   rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
 
 variable (K V) in
-theorem lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank [Module.Free K V]
+theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank [Module.Free K V]
     [Module.Finite K V] : lift.{u} #V = lift.{v} #K ^ lift.{u} (Module.rank K V) := by
   haveI := nontrivial_of_invariantBasisNumber K
   obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)
@@ -226,15 +226,22 @@ theorem lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank [Module.Free K
   rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
     lift_lift, lift_umax'] at this
 
-theorem cardinal_mk_eq_cardinal_mk_field_pow_rank (K V : Type u) [Ring K] [StrongRankCondition K]
+@[deprecated (since := "2024-11-10")]
+alias lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank :=
+  lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank
+
+theorem cardinalMk_eq_cardinalMk_field_pow_rank (K V : Type u) [Ring K] [StrongRankCondition K]
     [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
     #V = #K ^ Module.rank K V := by
-  simpa using lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank K V
+  simpa using lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V
+
+@[deprecated (since := "2024-11-10")]
+alias cardinal_mk_eq_cardinal_mk_field_pow_rank := cardinalMk_eq_cardinalMk_field_pow_rank
 
 variable (K V) in
 theorem cardinal_lt_aleph0_of_finiteDimensional [Finite K] [Module.Free K V] [Module.Finite K V] :
     #V < ℵ₀ := by
-  rw [← lift_lt_aleph0.{v, u}, lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank K V]
+  rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]
   exact power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K))
     (lift_lt_aleph0.2 (rank_lt_aleph0 K V))