F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
⊢ finrank F K * finrank K A = finrank F A
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
⊢ finrank F K * finrank K A = finrank F A
letI := nontrivial_of_invariantBasisNumber F
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
⊢ finrank F K * finrank K A = finrank F A
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
⊢ finrank F K * finrank K A = finrank F A
let b := Module.Free.chooseBasis F K
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
c : Basis (Module.Free.ChooseBasisIndex K A) K A := Module.Free.chooseBasis K A
⊢ finrank F K * finrank K A = finrank F A
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
⊢ finrank F K * finrank K A = finrank F A
let c := Module.Free.chooseBasis K A
no goals
F : Type u
K : Type v
A : Type w
inst✝¹³ : CommRing F
inst✝¹² : Ring K
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Algebra F K
inst✝⁹ : Module K A
inst✝⁸ : Module F A
inst✝⁷ : IsScalarTower F K A
inst✝⁶ : StrongRankCondition F
inst✝⁵ : StrongRankCondition K
inst✝⁴ : Module.Free F K
inst✝³ : Module.Free K A
inst✝² : Nontrivial K
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
c : Basis (Module.Free.ChooseBasisIndex K A) K A := Module.Free.chooseBasis K A
⊢ finrank F K * finrank K A = finrank F A
rw [finrank_eq_card_basis b, finrank_eq_card_basis c, finrank_eq_card_basis (b.smul c),
  Fintype.card_prod]