[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F
[PROOFSTEP]
let e := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F
[PROOFSTEP]
have : ∀ (c) (x : F), e c • x = c • x := by
  intro c x
  rw [Algebra.smul_def, Algebra.smul_def]
  congr
  refine' congr_fun (f := fun c => algebraMap Fqt F (e c)) _ c
  refine' IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ _ _ _ _ _ <;> intros <;>
    simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
      IsScalarTower.algebraMap_apply]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
⊢ ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
[PROOFSTEP]
intro c x
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑e c • x = c • x
[PROOFSTEP]
rw [Algebra.smul_def, Algebra.smul_def]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap ((fun x => Fqt) c) F) (↑e c) * x = ↑(algebraMap (RatFunc Fq) F) c * x
[PROOFSTEP]
congr
[GOAL]
case e_a
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap ((fun x => Fqt) c) F) (↑e c) = ↑(algebraMap (RatFunc Fq) F) c
[PROOFSTEP]
refine' congr_fun (f := fun c => algebraMap Fqt F (e c)) _ c
[GOAL]
case e_a
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ (fun c => ↑(algebraMap Fqt F) (↑e c)) = ↑(algebraMap (RatFunc Fq) F)
[PROOFSTEP]
refine' IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ _ _ _ _ _
[GOAL]
case e_a.refine'_1
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap Fqt F) (↑e 1) = 1
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_2
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap (RatFunc Fq) F) 1 = 1
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_3
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ∀ (a b : RatFunc Fq), ↑(algebraMap Fqt F) (↑e (a * b)) = ↑(algebraMap Fqt F) (↑e a) * ↑(algebraMap Fqt F) (↑e b)
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_4
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ∀ (a b : RatFunc Fq),
    ↑(algebraMap (RatFunc Fq) F) (a * b) = ↑(algebraMap (RatFunc Fq) F) a * ↑(algebraMap (RatFunc Fq) F) b
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ∀ (a : Fq[X]),
    ↑(algebraMap Fqt F) (↑e (↑(algebraMap Fq[X] (RatFunc Fq)) a)) =
      ↑(algebraMap (RatFunc Fq) F) (↑(algebraMap Fq[X] (RatFunc Fq)) a)
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_1
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap Fqt F) (↑e 1) = 1
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_2
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ ↑(algebraMap (RatFunc Fq) F) 1 = 1
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_3
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
a✝ b✝ : RatFunc Fq
⊢ ↑(algebraMap Fqt F) (↑e (a✝ * b✝)) = ↑(algebraMap Fqt F) (↑e a✝) * ↑(algebraMap Fqt F) (↑e b✝)
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_4
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
a✝ b✝ : RatFunc Fq
⊢ ↑(algebraMap (RatFunc Fq) F) (a✝ * b✝) = ↑(algebraMap (RatFunc Fq) F) a✝ * ↑(algebraMap (RatFunc Fq) F) b✝
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
a✝ : Fq[X]
⊢ ↑(algebraMap Fqt F) (↑e (↑(algebraMap Fq[X] (RatFunc Fq)) a✝)) =
    ↑(algebraMap (RatFunc Fq) F) (↑(algebraMap Fq[X] (RatFunc Fq)) a✝)
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F
[PROOFSTEP]
constructor
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
⊢ FunctionField Fq F → FiniteDimensional Fqt F
[PROOFSTEP]
intro h
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
⊢ FiniteDimensional Fqt F → FunctionField Fq F
[PROOFSTEP]
intro h
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FunctionField Fq F
⊢ FiniteDimensional Fqt F
[PROOFSTEP]
let b := FiniteDimensional.finBasis (RatFunc Fq) F
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FunctionField Fq F
b : Basis (Fin (FiniteDimensional.finrank (RatFunc Fq) F)) (RatFunc Fq) F := FiniteDimensional.finBasis (RatFunc Fq) F
⊢ FiniteDimensional Fqt F
[PROOFSTEP]
exact FiniteDimensional.of_fintype_basis (b.mapCoeffs e this)
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FiniteDimensional Fqt F
⊢ FunctionField Fq F
[PROOFSTEP]
let b := FiniteDimensional.finBasis Fqt F
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
⊢ FunctionField Fq F
[PROOFSTEP]
refine' FiniteDimensional.of_fintype_basis (b.mapCoeffs e.symm _)
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
⊢ ∀ (c : Fqt) (x : F), ↑↑(AlgEquiv.symm e) c • x = c • x
[PROOFSTEP]
intro c x
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
c : Fqt
x : F
⊢ ↑↑(AlgEquiv.symm e) c • x = c • x
[PROOFSTEP]
convert (this (e.symm c) x).symm
[GOAL]
case h.e'_3.h.e'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), ↑e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
c : Fqt
x : F
⊢ c = ↑e (↑(AlgEquiv.symm e) c)
[PROOFSTEP]
simp only [e.apply_symm_apply]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] F)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(RingHom.comp (algebraMap (RatFunc Fq) F) (algebraMap Fq[X] (RatFunc Fq)))
[PROOFSTEP]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F })
[PROOFSTEP]
have hinj : Function.Injective (⇑(algebraMap Fq[X] F)) :=
  by
  rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
  exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] F)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(RingHom.comp (algebraMap (RatFunc Fq) F) (algebraMap Fq[X] (RatFunc Fq)))
[PROOFSTEP]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
⊢ Function.Injective ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F })
[PROOFSTEP]
rw [injective_iff_map_eq_zero (algebraMap Fq[X] (↥(ringOfIntegers Fq F)))]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
⊢ ∀ (a : Fq[X]), ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) a = 0 → a = 0
[PROOFSTEP]
intro p hp
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
p : Fq[X]
hp : ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p = 0
⊢ p = 0
[PROOFSTEP]
rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp 
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
p : Fq[X]
hp : ↑(↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p) = 0
⊢ p = 0
[PROOFSTEP]
rw [injective_iff_map_eq_zero (algebraMap Fq[X] F)] at hinj 
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : ∀ (a : Fq[X]), ↑(algebraMap Fq[X] F) a = 0 → a = 0
p : Fq[X]
hp : ↑(↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p) = 0
⊢ p = 0
[PROOFSTEP]
exact hinj p hp
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ ¬IsField { x // x ∈ ringOfIntegers Fq F }
[PROOFSTEP]
simpa [← (IsIntegralClosure.isIntegral_algebra Fq[X] F).isField_iff_isField (algebraMap_injective Fq F)] using
  Polynomial.not_isField Fq
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
⊢ ↑(↑Multiplicative.ofAdd (RatFunc.intDegree 1)) = 1
[PROOFSTEP]
rw [RatFunc.intDegree_one, ofAdd_zero, WithZero.coe_one]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y
[PROOFSTEP]
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj, ← ofAdd_add,
  RatFunc.intDegree_mul hx hy]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [hx, zero_add]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ max 0 (inftyValuationDef Fq y)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq y))]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [hy, add_zero]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ max 0 (inftyValuationDef Fq x)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq x))]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hxy : x + y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos hxy]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
exact zero_le'
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy, if_neg hxy]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x + y))) ≤
    max ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x)) ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [le_max_iff, WithZero.coe_le_coe, Multiplicative.ofAdd_le, WithZero.coe_le_coe, Multiplicative.ofAdd_le, ←
  le_max_iff]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ RatFunc.intDegree (x + y) ≤ max (RatFunc.intDegree x) (RatFunc.intDegree y)
[PROOFSTEP]
exact RatFunc.intDegree_add_le hy hxy
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x : RatFunc Fq
hx : x ≠ 0
⊢ inftyValuationDef Fq x = ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))
[PROOFSTEP]
rw [inftyValuationDef, if_neg hx]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
⊢ inftyValuationDef Fq (↑RatFunc.C k) = ↑(↑Multiplicative.ofAdd 0)
[PROOFSTEP]
have hCk : RatFunc.C k ≠ 0 := (map_ne_zero _).mpr hk
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
hCk : ↑RatFunc.C k ≠ 0
⊢ inftyValuationDef Fq (↑RatFunc.C k) = ↑(↑Multiplicative.ofAdd 0)
[PROOFSTEP]
rw [inftyValuationDef, if_neg hCk, RatFunc.intDegree_C]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
⊢ inftyValuationDef Fq RatFunc.X = ↑(↑Multiplicative.ofAdd 1)
[PROOFSTEP]
rw [inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ inftyValuationDef Fq (↑(algebraMap Fq[X] (RatFunc Fq)) p) = ↑(↑Multiplicative.ofAdd ↑(Polynomial.natDegree p))
[PROOFSTEP]
have hp' : algebraMap Fq[X] (RatFunc Fq) p ≠ 0 := by rw [Ne.def, RatFunc.algebraMap_eq_zero_iff]; exact hp
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ ↑(algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
[PROOFSTEP]
rw [Ne.def, RatFunc.algebraMap_eq_zero_iff]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ ¬p = 0
[PROOFSTEP]
exact hp
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
hp' : ↑(algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
⊢ inftyValuationDef Fq (↑(algebraMap Fq[X] (RatFunc Fq)) p) = ↑(↑Multiplicative.ofAdd ↑(Polynomial.natDegree p))
[PROOFSTEP]
rw [inftyValuationDef, if_neg hp', RatFunc.intDegree_polynomial]
