[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
⊢ Module.rank R (ι →₀ M) = Cardinal.lift #ι * Cardinal.lift (Module.rank R M)
[PROOFSTEP]
obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
[GOAL]
case intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ Module.rank R (ι →₀ M) = Cardinal.lift #ι * Cardinal.lift (Module.rank R M)
[PROOFSTEP]
rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma, Cardinal.sum_const]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type v
⊢ Module.rank R (ι →₀ M) = #ι * Module.rank R M
[PROOFSTEP]
simp [rank_finsupp]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
⊢ Module.rank R (ι →₀ R) = Cardinal.lift #ι
[PROOFSTEP]
simp [rank_finsupp]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type u
⊢ Module.rank R (ι →₀ R) = #ι
[PROOFSTEP]
simp
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : Module.Free R M✝
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
[PROOFSTEP]
let B i := chooseBasis R (M i)
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : Module.Free R M✝
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
[PROOFSTEP]
let b : Basis _ R (⨁ i, M i) := DFinsupp.basis fun i => B i
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : Module.Free R M✝
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := DFinsupp.basis fun i => B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
[PROOFSTEP]
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = Cardinal.lift #m * Cardinal.lift #n
[PROOFSTEP]
cases nonempty_fintype m
[GOAL]
case intro
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
val✝ : Fintype m
⊢ Module.rank R (Matrix m n R) = Cardinal.lift #m * Cardinal.lift #n
[PROOFSTEP]
cases nonempty_fintype n
[GOAL]
case intro.intro
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Module.rank R (Matrix m n R) = Cardinal.lift #m * Cardinal.lift #n
[PROOFSTEP]
have h := (Matrix.stdBasis R m n).mk_eq_rank
[GOAL]
case intro.intro
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
h : Cardinal.lift #(m × n) = Cardinal.lift (Module.rank R (Matrix m n R))
⊢ Module.rank R (Matrix m n R) = Cardinal.lift #m * Cardinal.lift #n
[PROOFSTEP]
rw [← lift_lift.{max v w u, max v w}, lift_inj] at h 
[GOAL]
case intro.intro
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
h : Cardinal.lift #(m × n) = Module.rank R (Matrix m n R)
⊢ Module.rank R (Matrix m n R) = Cardinal.lift #m * Cardinal.lift #n
[PROOFSTEP]
simpa using h.symm
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = Cardinal.lift (#m * #n)
[PROOFSTEP]
rw [rank_matrix, lift_mul, lift_umax.{v, u}]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m n : Type u
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = #m * #n
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
[PROOFSTEP]
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
[GOAL]
case intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
[PROOFSTEP]
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := R) (M := N)
[GOAL]
case intro.mk.intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type w
bN : Basis fst✝ R N
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
[PROOFSTEP]
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
[GOAL]
R : Type u
M : Type v
N✝ : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module.Free R M
inst✝⁵ : AddCommGroup N✝
inst✝⁴ : Module R N✝
inst✝³ : Module.Free R N✝
N : Type v
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
⊢ Module.rank R (M ⊗[R] N) = Module.rank R M * Module.rank R N
[PROOFSTEP]
simp
