k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
letI : IsDomain R := (NoZeroSMulDivisors.algebraMap_injective R S).isDomain _
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
x✝ : FractionRing S
⊢ IsAlgebraic (FractionRing R) x✝
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
intro
no goals
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
x✝ : FractionRing S
⊢ IsAlgebraic (FractionRing R) x✝
exact
  (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    ((IsFractionRing.isAlgebraic_iff' R S (FractionRing S)).1 hS _)