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 : FiniteType (RingHom.comp g f)
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType 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 : FiniteType (RingHom.comp g f)
⊢ FiniteType g
let _ := 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 : FiniteType (RingHom.comp g f)
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra B C := toAlgebra g
⊢ FiniteType 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 : FiniteType (RingHom.comp g f)
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType g
let _ := 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 : FiniteType (RingHom.comp g f)
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra B C := toAlgebra g
x✝ : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ FiniteType 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 : FiniteType (RingHom.comp g f)
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra B C := toAlgebra g
⊢ FiniteType g
let _ := (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 : FiniteType (RingHom.comp g f)
x✝³ : Algebra A B := toAlgebra f
x✝² : Algebra B C := toAlgebra g
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
⊢ FiniteType 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 : FiniteType (RingHom.comp g f)
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra B C := toAlgebra g
x✝ : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ FiniteType g
let _ : 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 : FiniteType (RingHom.comp g f)
x✝⁴ : Algebra A B := toAlgebra f
x✝³ : Algebra B C := toAlgebra g
x✝² : Algebra A C := toAlgebra (RingHom.comp g f)
x✝¹ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
x✝ : Algebra.FiniteType A C := h
⊢ FiniteType 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 : FiniteType (RingHom.comp g f)
x✝³ : Algebra A B := toAlgebra f
x✝² : Algebra B C := toAlgebra g
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
⊢ FiniteType g
let _ : Algebra.FiniteType 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 : FiniteType (RingHom.comp g f)
x✝⁴ : Algebra A B := toAlgebra f
x✝³ : Algebra B C := toAlgebra g
x✝² : Algebra A C := toAlgebra (RingHom.comp g f)
x✝¹ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
x✝ : Algebra.FiniteType A C := h
⊢ FiniteType g
exact Algebra.FiniteType.of_restrictScalars_finiteType A B C