Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 039a089

Browse files
eric-wiesereric-wieser
committed
refactor(linear_algebra/dimension): use rank in lemma names instead of dim (#18741)
The `dim` name is left from the previous name of the function, `vector_space.dim`. When that was merged with `module.rank` in #7322, we left renaming the existing lemmas as future work. This commit was made by replacing `(\b|(?<=_))dim(\b|(?=_))` with `rank` in the `dimension` and `finite_dimensional` files, and then manually fixing downstream breakages; it's important not to rename `power_basis.dim` at the same time! Deciding whether to move some of these to the `module` namespace is left as future work, the diff is already big enough.
1 parent 0ac3057 commit 039a089

26 files changed

Lines changed: 396 additions & 391 deletions

‎archive/sensitivity.lean‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -230,15 +230,15 @@ since this cardinal is finite, as a natural number in `finrank_V` -/
230230

231231
lemma dim_V : module.rank ℝ (V n) = 2^n :=
232232
have module.rank ℝ (V n) = (2^n : ℕ),
233-
by { rw [dim_eq_card_basis (dual_bases_e_ε _).basis, Q.card]; apply_instance },
233+
by { rw [rank_eq_card_basis (dual_bases_e_ε _).basis, Q.card]; apply_instance },
234234
by assumption_mod_cast
235235

236236
instance : finite_dimensional ℝ (V n) :=
237237
finite_dimensional.of_fintype_basis (dual_bases_e_ε _).basis
238238

239239
lemma finrank_V : finrank ℝ (V n) = 2^n :=
240240
have _ := @dim_V n,
241-
by rw ←finrank_eq_dim at this; assumption_mod_cast
241+
by rw ←finrank_eq_rank at this; assumption_mod_cast
242242

243243
/-! ### The linear map -/
244244

@@ -359,25 +359,25 @@ begin
359359
let img := (g m).range,
360360
suffices : 0 < dim (W ⊓ img),
361361
{ simp only [exists_prop],
362-
exact_mod_cast exists_mem_ne_zero_of_dim_pos this },
362+
exact_mod_cast exists_mem_ne_zero_of_rank_pos this },
363363
have dim_le : dim (W ⊔ img) ≤ 2^(m + 1),
364-
{ convert ← dim_submodule_le (W ⊔ img),
364+
{ convert ← rank_submodule_le (W ⊔ img),
365365
apply dim_V },
366366
have dim_add : dim (W ⊔ img) + dim (W ⊓ img) = dim W + 2^m,
367-
{ convert ← dim_sup_add_dim_inf_eq W img,
368-
rw ← dim_eq_of_injective (g m) g_injective,
367+
{ convert ← rank_sup_add_rank_inf_eq W img,
368+
rw ← rank_eq_of_injective (g m) g_injective,
369369
apply dim_V },
370370
have dimW : dim W = card H,
371371
{ have li : linear_independent ℝ (H.restrict e),
372372
{ convert (dual_bases_e_ε _).basis.linear_independent.comp _ subtype.val_injective,
373373
rw (dual_bases_e_ε _).coe_basis },
374-
have hdW := dim_span li,
374+
have hdW := rank_span li,
375375
rw set.range_restrict at hdW,
376376
convert hdW,
377377
rw [← (dual_bases_e_ε _).coe_basis, cardinal.mk_image_eq (dual_bases_e_ε _).basis.injective,
378378
cardinal.mk_fintype] },
379-
rw ← finrank_eq_dim ℝ at ⊢ dim_le dim_add dimW,
380-
rw [← finrank_eq_dim ℝ, ← finrank_eq_dim ℝ] at dim_add,
379+
rw ← finrank_eq_rank ℝ at ⊢ dim_le dim_add dimW,
380+
rw [← finrank_eq_rank ℝ, ← finrank_eq_rank ℝ] at dim_add,
381381
norm_cast at ⊢ dim_le dim_add dimW,
382382
rw pow_succ' at dim_le,
383383
rw set.to_finset_card at hH,

‎src/algebra/linear_recurrence.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -174,10 +174,10 @@ section strong_rank_condition
174174
variables {α : Type*} [comm_ring α] [strong_rank_condition α] (E : linear_recurrence α)
175175

176176
/-- The dimension of `E.sol_space` is `E.order`. -/
177-
lemma sol_space_dim : module.rank α E.sol_space = E.order :=
177+
lemma sol_space_rank : module.rank α E.sol_space = E.order :=
178178
begin
179179
letI := nontrivial_of_invariant_basis_number α,
180-
exact @dim_fin_fun α _ _ E.order ▸ E.to_init.dim_eq
180+
exact @rank_fin_fun α _ _ E.order ▸ E.to_init.rank_eq
181181
end
182182

183183
end strong_rank_condition

‎src/algebra/quaternion.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -309,13 +309,13 @@ basis.of_equiv_fun $ linear_equiv_tuple c₁ c₂
309309
instance : module.finite R ℍ[R, c₁, c₂] := module.finite.of_basis (basis_one_i_j_k c₁ c₂)
310310
instance : module.free R ℍ[R, c₁, c₂] := module.free.of_basis (basis_one_i_j_k c₁ c₂)
311311

312-
lemma dim_eq_four [strong_rank_condition R] : module.rank R ℍ[R, c₁, c₂] = 4 :=
313-
by { rw [dim_eq_card_basis (basis_one_i_j_k c₁ c₂), fintype.card_fin], norm_num }
312+
lemma rank_eq_four [strong_rank_condition R] : module.rank R ℍ[R, c₁, c₂] = 4 :=
313+
by { rw [rank_eq_card_basis (basis_one_i_j_k c₁ c₂), fintype.card_fin], norm_num }
314314

315315
lemma finrank_eq_four [strong_rank_condition R] : finite_dimensional.finrank R ℍ[R, c₁, c₂] = 4 :=
316316
have cardinal.to_nat 4 = 4,
317317
by rw [←cardinal.to_nat_cast 4, nat.cast_bit0, nat.cast_bit0, nat.cast_one],
318-
by rw [finite_dimensional.finrank, dim_eq_four, this]
318+
by rw [finite_dimensional.finrank, rank_eq_four, this]
319319

320320
end
321321

@@ -631,8 +631,8 @@ lemma smul_coe : x • (y : ℍ[R]) = ↑(x * y) := quaternion_algebra.smul_coe
631631
instance : module.finite R ℍ[R] := quaternion_algebra.module.finite _ _
632632
instance : module.free R ℍ[R] := quaternion_algebra.module.free _ _
633633

634-
lemma dim_eq_four [strong_rank_condition R] : module.rank R ℍ[R] = 4 :=
635-
quaternion_algebra.dim_eq_four _ _
634+
lemma rank_eq_four [strong_rank_condition R] : module.rank R ℍ[R] = 4 :=
635+
quaternion_algebra.rank_eq_four _ _
636636

637637
lemma finrank_eq_four [strong_rank_condition R] : finite_dimensional.finrank R ℍ[R] = 4 :=
638638
quaternion_algebra.finrank_eq_four _ _

‎src/analysis/inner_product_space/projection.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1047,7 +1047,7 @@ lemma submodule.finrank_add_inf_finrank_orthogonal {K₁ K₂ : submodule 𝕜 E
10471047
begin
10481048
haveI := submodule.finite_dimensional_of_le h,
10491049
haveI := proper_is_R_or_C 𝕜 K₁,
1050-
have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁ᗮ ⊓ K₂),
1050+
have hd := submodule.rank_sup_add_rank_inf_eq K₁ (K₁ᗮ ⊓ K₂),
10511051
rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
10521052
submodule.sup_orthogonal_inf_of_complete_space h] at hd,
10531053
rw add_zero at hd,

‎src/data/complex/module.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -157,11 +157,11 @@ instance : finite_dimensional ℝ ℂ := of_fintype_basis basis_one_I
157157
@[simp] lemma finrank_real_complex : finite_dimensional.finrank ℝ ℂ = 2 :=
158158
by rw [finrank_eq_card_basis basis_one_I, fintype.card_fin]
159159

160-
@[simp] lemma dim_real_complex : module.rank ℝ ℂ = 2 :=
161-
by simp [← finrank_eq_dim, finrank_real_complex]
160+
@[simp] lemma rank_real_complex : module.rank ℝ ℂ = 2 :=
161+
by simp [← finrank_eq_rank, finrank_real_complex]
162162

163-
lemma {u} dim_real_complex' : cardinal.lift.{u} (module.rank ℝ ℂ) = 2 :=
164-
by simp [← finrank_eq_dim, finrank_real_complex, bit0]
163+
lemma {u} rank_real_complex' : cardinal.lift.{u} (module.rank ℝ ℂ) = 2 :=
164+
by simp [← finrank_eq_rank, finrank_real_complex, bit0]
165165

166166
/-- `fact` version of the dimension of `ℂ` over `ℝ`, locally useful in the definition of the
167167
circle. -/
@@ -199,10 +199,10 @@ instance finite_dimensional.complex_to_real (E : Type*) [add_comm_group E] [modu
199199
[finite_dimensional ℂ E] : finite_dimensional ℝ E :=
200200
finite_dimensional.trans ℝ ℂ E
201201

202-
lemma dim_real_of_complex (E : Type*) [add_comm_group E] [module ℂ E] :
202+
lemma rank_real_of_complex (E : Type*) [add_comm_group E] [module ℂ E] :
203203
module.rank ℝ E = 2 * module.rank ℂ E :=
204204
cardinal.lift_inj.1 $
205-
by { rw [← dim_mul_dim' ℝ ℂ E, complex.dim_real_complex], simp [bit0] }
205+
by { rw [← rank_mul_rank' ℝ ℂ E, complex.rank_real_complex], simp [bit0] }
206206

207207
lemma finrank_real_of_complex (E : Type*) [add_comm_group E] [module ℂ E] :
208208
finite_dimensional.finrank ℝ E = 2 * finite_dimensional.finrank ℂ E :=

‎src/field_theory/adjoin.lean‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ For example, `algebra.adjoin K {x}` might not include `x⁻¹`.
1919
## Main results
2020
2121
- `adjoin_adjoin_left`: adjoining S and then T is the same as adjoining `S ∪ T`.
22-
- `bot_eq_top_of_dim_adjoin_eq_one`: if `F⟮x⟯` has dimension `1` over `F` for every `x`
22+
- `bot_eq_top_of_rank_adjoin_eq_one`: if `F⟮x⟯` has dimension `1` over `F` for every `x`
2323
in `E` then `F = E`
2424
2525
## Notation
@@ -528,30 +528,30 @@ adjoin_simple_eq_bot_iff.mpr (coe_int_mem ⊥ n)
528528
@[simp] lemma adjoin_nat (n : ℕ) : F⟮(n : E)⟯ = ⊥ :=
529529
adjoin_simple_eq_bot_iff.mpr (coe_nat_mem ⊥ n)
530530

531-
section adjoin_dim
531+
section adjoin_rank
532532
open finite_dimensional module
533533

534534
variables {K L : intermediate_field F E}
535535

536-
@[simp] lemma dim_eq_one_iff : module.rank F K = 1 ↔ K = ⊥ :=
537-
by rw [← to_subalgebra_eq_iff, ← dim_eq_dim_subalgebra,
538-
subalgebra.dim_eq_one_iff, bot_to_subalgebra]
536+
@[simp] lemma rank_eq_one_iff : module.rank F K = 1 ↔ K = ⊥ :=
537+
by rw [← to_subalgebra_eq_iff, ← rank_eq_rank_subalgebra,
538+
subalgebra.rank_eq_one_iff, bot_to_subalgebra]
539539

540540
@[simp] lemma finrank_eq_one_iff : finrank F K = 1 ↔ K = ⊥ :=
541541
by rw [← to_subalgebra_eq_iff, ← finrank_eq_finrank_subalgebra,
542542
subalgebra.finrank_eq_one_iff, bot_to_subalgebra]
543543

544-
@[simp] lemma dim_bot : module.rank F (⊥ : intermediate_field F E) = 1 :=
545-
by rw dim_eq_one_iff
544+
@[simp] lemma rank_bot : module.rank F (⊥ : intermediate_field F E) = 1 :=
545+
by rw rank_eq_one_iff
546546

547547
@[simp] lemma finrank_bot : finrank F (⊥ : intermediate_field F E) = 1 :=
548548
by rw finrank_eq_one_iff
549549

550-
lemma dim_adjoin_eq_one_iff : module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
551-
iff.trans dim_eq_one_iff adjoin_eq_bot_iff
550+
lemma rank_adjoin_eq_one_iff : module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
551+
iff.trans rank_eq_one_iff adjoin_eq_bot_iff
552552

553-
lemma dim_adjoin_simple_eq_one_iff : module.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : intermediate_field F E) :=
554-
by { rw dim_adjoin_eq_one_iff, exact set.singleton_subset_iff }
553+
lemma rank_adjoin_simple_eq_one_iff : module.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : intermediate_field F E) :=
554+
by { rw rank_adjoin_eq_one_iff, exact set.singleton_subset_iff }
555555

556556
lemma finrank_adjoin_eq_one_iff : finrank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
557557
iff.trans finrank_eq_one_iff adjoin_eq_bot_iff
@@ -560,12 +560,12 @@ lemma finrank_adjoin_simple_eq_one_iff : finrank F F⟮α⟯ = 1 ↔ α ∈ (⊥
560560
by { rw [finrank_adjoin_eq_one_iff], exact set.singleton_subset_iff }
561561

562562
/-- If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`. -/
563-
lemma bot_eq_top_of_dim_adjoin_eq_one (h : ∀ x : E, module.rank F F⟮x⟯ = 1) :
563+
lemma bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, module.rank F F⟮x⟯ = 1) :
564564
(⊥ : intermediate_field F E) = ⊤ :=
565565
begin
566566
ext,
567567
rw iff_true_right intermediate_field.mem_top,
568-
exact dim_adjoin_simple_eq_one_iff.mp (h x),
568+
exact rank_adjoin_simple_eq_one_iff.mp (h x),
569569
end
570570

571571
lemma bot_eq_top_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) :
@@ -576,9 +576,9 @@ begin
576576
exact finrank_adjoin_simple_eq_one_iff.mp (h x),
577577
end
578578

579-
lemma subsingleton_of_dim_adjoin_eq_one (h : ∀ x : E, module.rank F F⟮x⟯ = 1) :
579+
lemma subsingleton_of_rank_adjoin_eq_one (h : ∀ x : E, module.rank F F⟮x⟯ = 1) :
580580
subsingleton (intermediate_field F E) :=
581-
subsingleton_of_bot_eq_top (bot_eq_top_of_dim_adjoin_eq_one h)
581+
subsingleton_of_bot_eq_top (bot_eq_top_of_rank_adjoin_eq_one h)
582582

583583
lemma subsingleton_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) :
584584
subsingleton (intermediate_field F E) :=
@@ -596,7 +596,7 @@ lemma subsingleton_of_finrank_adjoin_le_one [finite_dimensional F E]
596596
(h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : subsingleton (intermediate_field F E) :=
597597
subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_le_one h)
598598

599-
end adjoin_dim
599+
end adjoin_rank
600600
end adjoin_intermediate_field_lattice
601601

602602
section adjoin_integral_element

‎src/field_theory/finite/polynomial.lean‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -177,13 +177,13 @@ end comm_ring
177177

178178
variables [field K]
179179

180-
lemma dim_R [fintype σ] : module.rank K (R σ K) = fintype.card (σ → K) :=
180+
lemma rank_R [fintype σ] : module.rank K (R σ K) = fintype.card (σ → K) :=
181181
calc module.rank K (R σ K) =
182182
module.rank K (↥{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} →₀ K) :
183-
linear_equiv.dim_eq
183+
linear_equiv.rank_eq
184184
(finsupp.supported_equiv_finsupp {s : σ →₀ ℕ | ∀n:σ, s n ≤ fintype.card K - 1 })
185185
... = #{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} :
186-
by rw [finsupp.dim_eq, dim_self, mul_one]
186+
by rw [finsupp.rank_eq, rank_self, mul_one]
187187
... = #{s : σ → ℕ | ∀ (n : σ), s n < fintype.card K } :
188188
begin
189189
refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_finite $ assume f, _⟩,
@@ -199,11 +199,12 @@ calc module.rank K (R σ K) =
199199
... = fintype.card (σ → K) : cardinal.mk_fintype _
200200

201201
instance [finite σ] : finite_dimensional K (R σ K) :=
202-
by { casesI nonempty_fintype σ, exact is_noetherian.iff_fg.1 (is_noetherian.iff_dim_lt_aleph_0.mpr $
203-
by simpa only [dim_R] using cardinal.nat_lt_aleph_0 (fintype.card (σ → K))) }
202+
by { casesI nonempty_fintype σ,
203+
exact is_noetherian.iff_fg.1 (is_noetherian.iff_rank_lt_aleph_0.mpr $
204+
by simpa only [rank_R] using cardinal.nat_lt_aleph_0 (fintype.card (σ → K))) }
204205

205206
lemma finrank_R [fintype σ] : finite_dimensional.finrank K (R σ K) = fintype.card (σ → K) :=
206-
finite_dimensional.finrank_eq_of_dim_eq (dim_R σ K)
207+
finite_dimensional.finrank_eq_of_rank_eq (rank_R σ K)
207208

208209
lemma range_evalᵢ [finite σ] : (evalᵢ σ K).range = ⊤ :=
209210
begin

‎src/field_theory/finiteness.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,10 @@ variables {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module
2424
A module over a division ring is noetherian if and only if
2525
its dimension (as a cardinal) is strictly less than the first infinite cardinal `ℵ₀`.
2626
-/
27-
lemma iff_dim_lt_aleph_0 : is_noetherian K V ↔ module.rank K V < ℵ₀ :=
27+
lemma iff_rank_lt_aleph_0 : is_noetherian K V ↔ module.rank K V < ℵ₀ :=
2828
begin
2929
let b := basis.of_vector_space K V,
30-
rw [← b.mk_eq_dim'', lt_aleph_0_iff_set_finite],
30+
rw [← b.mk_eq_rank'', lt_aleph_0_iff_set_finite],
3131
split,
3232
{ introI,
3333
exact finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },
@@ -42,15 +42,15 @@ variables (K V)
4242

4343
/-- The dimension of a noetherian module over a division ring, as a cardinal,
4444
is strictly less than the first infinite cardinal `ℵ₀`. -/
45-
lemma dim_lt_aleph_0 : ∀ [is_noetherian K V], module.rank K V < ℵ₀ :=
46-
is_noetherian.iff_dim_lt_aleph_0.1
45+
lemma rank_lt_aleph_0 : ∀ [is_noetherian K V], module.rank K V < ℵ₀ :=
46+
is_noetherian.iff_rank_lt_aleph_0.1
4747

4848
variables {K V}
4949

5050
/-- In a noetherian module over a division ring, all bases are indexed by a finite type. -/
5151
noncomputable def fintype_basis_index {ι : Type*} [is_noetherian K V] (b : basis ι K V) :
5252
fintype ι :=
53-
b.fintype_index_of_dim_lt_aleph_0 (dim_lt_aleph_0 K V)
53+
b.fintype_index_of_rank_lt_aleph_0 (rank_lt_aleph_0 K V)
5454

5555
/-- In a noetherian module over a division ring,
5656
`basis.of_vector_space` is indexed by a finite type. -/
@@ -61,7 +61,7 @@ fintype_basis_index (basis.of_vector_space K V)
6161
if a basis is indexed by a set, that set is finite. -/
6262
lemma finite_basis_index {ι : Type*} {s : set ι} [is_noetherian K V] (b : basis s K V) :
6363
s.finite :=
64-
b.finite_index_of_dim_lt_aleph_0 (dim_lt_aleph_0 K V)
64+
b.finite_index_of_rank_lt_aleph_0 (rank_lt_aleph_0 K V)
6565

6666
variables (K V)
6767

@@ -103,8 +103,8 @@ begin
103103
{ introI h,
104104
exact ⟨⟨finset_basis_index K V, by { convert (finset_basis K V).span_eq, simp }⟩⟩ },
105105
{ rintros ⟨s, hs⟩,
106-
rw [is_noetherian.iff_dim_lt_aleph_0, ← dim_top, ← hs],
107-
exact lt_of_le_of_lt (dim_span_le _) s.finite_to_set.lt_aleph_0 }
106+
rw [is_noetherian.iff_rank_lt_aleph_0, ← rank_top, ← hs],
107+
exact lt_of_le_of_lt (rank_span_le _) s.finite_to_set.lt_aleph_0 }
108108
end
109109

110110
end is_noetherian

‎src/field_theory/fixed.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -232,10 +232,10 @@ theorem minpoly_eq_minpoly :
232232
minpoly.eq_of_irreducible_of_monic (minpoly.irreducible G F x)
233233
(minpoly.eval₂ G F x) (minpoly.monic G F x)
234234

235-
lemma dim_le_card : module.rank (fixed_points.subfield G F) F ≤ fintype.card G :=
236-
dim_le $ λ s hs, by simpa only [dim_fun', cardinal.mk_coe_finset, finset.coe_sort_coe,
235+
lemma rank_le_card : module.rank (fixed_points.subfield G F) F ≤ fintype.card G :=
236+
rank_le $ λ s hs, by simpa only [rank_fun', cardinal.mk_coe_finset, finset.coe_sort_coe,
237237
cardinal.lift_nat_cast, cardinal.nat_cast_le]
238-
using cardinal_lift_le_dim_of_linear_independent'
238+
using cardinal_lift_le_rank_of_linear_independent'
239239
(linear_independent_smul_of_linear_independent G F hs)
240240

241241
end fintype
@@ -262,15 +262,15 @@ instance separable : is_separable (fixed_points.subfield G F) F :=
262262
exact polynomial.separable_prod_X_sub_C_iff.2 (injective_of_quotient_stabilizer G x) }⟩
263263

264264
instance : finite_dimensional (subfield G F) F :=
265-
by { casesI nonempty_fintype G, exact is_noetherian.iff_fg.1 (is_noetherian.iff_dim_lt_aleph_0.2 $
266-
(dim_le_card G F).trans_lt $ cardinal.nat_lt_aleph_0 _) }
265+
by { casesI nonempty_fintype G, exact is_noetherian.iff_fg.1 (is_noetherian.iff_rank_lt_aleph_0.2 $
266+
(rank_le_card G F).trans_lt $ cardinal.nat_lt_aleph_0 _) }
267267

268268
end finite
269269

270270
lemma finrank_le_card [fintype G] : finrank (subfield G F) F ≤ fintype.card G :=
271271
begin
272-
rw [← cardinal.nat_cast_le, finrank_eq_dim],
273-
apply dim_le_card,
272+
rw [← cardinal.nat_cast_le, finrank_eq_rank],
273+
apply rank_le_card,
274274
end
275275

276276
end fixed_points

‎src/field_theory/intermediate_field.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -472,7 +472,7 @@ left K F L
472472
instance finite_dimensional_right [finite_dimensional K L] : finite_dimensional F L :=
473473
right K F L
474474

475-
@[simp] lemma dim_eq_dim_subalgebra :
475+
@[simp] lemma rank_eq_rank_subalgebra :
476476
module.rank K F.to_subalgebra = module.rank K F := rfl
477477

478478
@[simp] lemma finrank_eq_finrank_subalgebra :

0 commit comments

Comments
 (0)