A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this : Algebra A B := toAlgebra f
⊢ Finite (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
⊢ Finite (RingHom.comp g f)
letI := f.toAlgebra
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this✝ : Algebra A B := toAlgebra f
this : Algebra B C := toAlgebra g
⊢ Finite (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this : Algebra A B := toAlgebra f
⊢ Finite (RingHom.comp g f)
letI := g.toAlgebra
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this✝¹ : Algebra A B := toAlgebra f
this✝ : Algebra B C := toAlgebra g
this : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ Finite (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this✝ : Algebra A B := toAlgebra f
this : Algebra B C := toAlgebra g
⊢ Finite (RingHom.comp g f)
letI := (g.comp f).toAlgebra
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite f
this✝¹ : Algebra A B := toAlgebra f
this✝ : Algebra B C := toAlgebra g
this : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ Finite (RingHom.comp g f)
letI : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 B := hf
⊢ Finite (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 (RingHom.comp g f)
letI : Module.Finite A B := hf
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 B := hf
this : Module.Finite B C := hg
⊢ Finite (RingHom.comp g f)
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 B := hf
⊢ Finite (RingHom.comp g f)
letI : Module.Finite B C := hg
no goals
A : Type u_3
B : Type u_1
C : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : Finite g
hf : Finite 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 B := hf
this : Module.Finite B C := hg
⊢ Finite (RingHom.comp g f)
exact Module.Finite.trans B C