case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A

case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
⊢ finrank F K * finrank K A = finrank F A
by_cases hA : FiniteDimensional K A
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
replace hA : FiniteDimensional K A := hA
no goals
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
rw [finrank_mul_finrank']
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ ¬FiniteDimensional F A
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
rw [finrank_of_infinite_dimensional hA, MulZeroClass.mul_zero, finrank_of_infinite_dimensional]
no goals
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ ¬FiniteDimensional F A
exact mt (@right F K A _ _ _ _ _ _ _) hA