A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this : Algebra A B := toAlgebra f
⊢ Finite g
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
⊢ Finite g
letI := f.toAlgebra
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝ : Algebra A B := toAlgebra f
this : Algebra B C := toAlgebra g
⊢ Finite g
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this : Algebra A B := toAlgebra f
⊢ Finite g
letI := g.toAlgebra
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝¹ : Algebra A B := toAlgebra f
this✝ : Algebra B C := toAlgebra g
this : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ Finite g
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝ : Algebra A B := toAlgebra f
this : Algebra B C := toAlgebra g
⊢ Finite g
letI := (g.comp f).toAlgebra
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝² : Algebra A B := toAlgebra f
this✝¹ : Algebra B C := toAlgebra g
this✝ : Algebra A C := toAlgebra (RingHom.comp g f)
this : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
⊢ Finite g
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝¹ : Algebra A B := toAlgebra f
this✝ : Algebra B C := toAlgebra g
this : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ Finite g
letI : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝³ : Algebra A B := toAlgebra f
this✝² : Algebra B C := toAlgebra g
this✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
this✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
this : Module.Finite A C := h
⊢ Finite g
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝² : Algebra A B := toAlgebra f
this✝¹ : Algebra B C := toAlgebra g
this✝ : Algebra A C := toAlgebra (RingHom.comp g f)
this : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
⊢ Finite g
letI : Module.Finite A C := h
no goals
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : Finite (RingHom.comp g f)
this✝³ : Algebra A B := toAlgebra f
this✝² : Algebra B C := toAlgebra g
this✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
this✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
this : Module.Finite A C := h
⊢ Finite g
exact Module.Finite.of_restrictScalars_finite A B C