[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have hST : Function.Injective (algebraMap (adjoin K ({ x } : Set S)) S) := Subtype.coe_injective
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have hx' : IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({ x } : Set S)) :=
  by
  apply (isIntegral_algebraMap_iff hST).mp
  convert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
[PROOFSTEP]
apply (isIntegral_algebraMap_iff hST).mp
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ IsIntegral K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
[PROOFSTEP]
convert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have minpoly_eq := minpoly.eq_of_algebraMap_eq hST hx' rfl
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
apply
  @Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K { x }) fun i => ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
[GOAL]
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ LinearIndependent K fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
have : LinearIndependent K _ := linearIndependent_pow (⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K { x })
[GOAL]
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
this : LinearIndependent K fun i => { val := x, property := (_ : x ∈ adjoin K {x}) } ^ ↑i
⊢ LinearIndependent K fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
rwa [minpoly_eq] at this 
[GOAL]
case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ ⊤ ≤ Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
rintro ⟨y, hy⟩ _
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
have := hx'.mem_span_pow (y := ⟨y, hy⟩)
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
rw [minpoly_eq] at this 
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
apply this
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
rw [adjoin_singleton_eq_range_aeval] at hy 
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy✝ : y ∈ adjoin K {x}
hy : y ∈ AlgHom.range (aeval x)
a✝ : { val := y, property := hy✝ } ∈ ⊤
this :
  (∃ f, { val := y, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f, { val := y, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
[GOAL]
case hsp.mk.intro
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1
[PROOFSTEP]
use f
[GOAL]
case h
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
ext
[GOAL]
case h.a
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ↑{ val := ↑(aeval x) f, property := hy✝ } = ↑(↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f)
[PROOFSTEP]
exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K { x }) _
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
⊢ ↑(powerBasisAux hx) i = { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
rw [adjoin.powerBasisAux, Basis.mk_apply]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
intro i
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
let Q := X ^ n %ₘ minpoly R B.gen
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
have : B.gen ^ n = aeval B.gen Q :=
  by
  rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
  simp
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ B.gen ^ n = ↑(aeval B.gen) Q
[PROOFSTEP]
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ ↑(aeval B.gen) (X ^ n %ₘ minpoly R B.gen + minpoly R B.gen * (X ^ n /ₘ minpoly R B.gen)) = ↑(aeval B.gen) Q
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
by_cases hQ : Q = 0
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : Q = 0
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
simp [this, hQ, isIntegral_zero]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
have hlt : Q.natDegree < B.dim :=
  by
  rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map, natDegree_lt_natDegree_iff hQ]
  letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
  exact degree_modByMonic_lt _ (minpoly.monic hB)
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ natDegree Q < B.dim
[PROOFSTEP]
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map, natDegree_lt_natDegree_iff hQ]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ degree Q < degree (minpoly R B.gen)
[PROOFSTEP]
letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this✝ : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
this : Nontrivial R := Nontrivial.of_polynomial_ne hQ
⊢ degree Q < degree (minpoly R B.gen)
[PROOFSTEP]
exact degree_modByMonic_lt _ (minpoly.monic hB)
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
rw [this, aeval_eq_sum_range' hlt]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (Finset.sum (Finset.range B.dim) fun i => coeff Q i • B.gen ^ i)) i)
[PROOFSTEP]
simp only [LinearEquiv.map_sum, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finset.sum_apply']
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R
    (Finset.sum (Finset.range B.dim) fun x => ↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) x • B.gen ^ x)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun j hj => _
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j ∈ Finset.range B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) j • B.gen ^ j)) i)
[PROOFSTEP]
replace hj := Finset.mem_range.1 hj
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) j • B.gen ^ j)) i)
[PROOFSTEP]
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ← Algebra.smul_def,
  LinearEquiv.map_smul]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R
    (↑(↑(algebraMap R S) (coeff (X ^ n %ₘ minpoly R B.gen) ↑{ val := j, isLt := hj }) •
          ↑B.basis.repr (↑B.basis { val := j, isLt := hj }))
      i)
[PROOFSTEP]
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
by_cases hij : (⟨j, hj⟩ : Fin _) = i
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
simp only [hij, eq_self_iff_true, if_true]
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • 1)
[PROOFSTEP]
rw [Algebra.smul_def, mul_one]
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (↑(algebraMap R S) (coeff (X ^ n %ₘ minpoly R B.gen) j))
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : ¬{ val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
simp [hij, isIntegral_zero]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x * y)) i)
[PROOFSTEP]
intro i
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (x * y)) i)
[PROOFSTEP]
rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, LinearEquiv.map_sum, Finset.sum_apply']
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
⊢ IsIntegral R
    (Finset.sum (Finset.univ ×ˢ Finset.univ) fun k =>
      ↑(↑B.basis.repr (↑(↑B.basis.repr x) k.fst • ↑B.basis k.fst * ↑(↑B.basis.repr y) k.snd • ↑B.basis k.snd)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun I _ => _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R
    (↑(↑B.basis.repr (↑(↑B.basis.repr x) I.fst • ↑B.basis I.fst * ↑(↑B.basis.repr y) I.snd • ↑B.basis I.snd)) i)
[PROOFSTEP]
simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finsupp.coe_smul,
  Pi.smul_apply, id.smul_eq_mul]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R
    ((↑(↑B.basis.repr y) I.snd • ↑(↑B.basis.repr x) I.fst • ↑(↑B.basis.repr (↑B.basis I.fst * ↑B.basis I.snd))) i)
[PROOFSTEP]
refine' isIntegral_mul (hy _) (isIntegral_mul (hx _) _)
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R (↑(↑B.basis.repr (↑B.basis I.fst * ↑B.basis I.snd)) i)
[PROOFSTEP]
simp only [coe_basis, ← pow_add]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ (↑I.fst + ↑I.snd))) i)
[PROOFSTEP]
refine' repr_gen_pow_isIntegral hB hmin _ _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
revert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
    ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
refine'
  Nat.case_strong_induction_on (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i)) n _
    fun n hn => _
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
    0
[PROOFSTEP]
intro _ i
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (x ^ 0)) i)
[PROOFSTEP]
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow, B.basis.repr_self_apply]
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R (if { val := 0, isLt := (_ : 0 < B.dim) } = i then 1 else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
h✝ : { val := 0, isLt := (_ : 0 < B.dim) } = i
⊢ IsIntegral R 1
[PROOFSTEP]
exact isIntegral_one
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
h✝ : ¬{ val := 0, isLt := (_ : 0 < B.dim) } = i
⊢ IsIntegral R 0
[PROOFSTEP]
exact isIntegral_zero
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
    (Nat.succ n)
[PROOFSTEP]
intro hx
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ Nat.succ n)) i)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x * x ^ n)) i)
[PROOFSTEP]
exact repr_mul_isIntegral hB hx (fun _ => hn _ le_rfl (fun _ => hx _) _) hmin
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (Basis.toMatrix B.basis (↑B'.basis) i j)
[PROOFSTEP]
intro i j
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (Basis.toMatrix B.basis (↑B'.basis) i j)
[PROOFSTEP]
rw [B.basis.toMatrix_apply, B'.coe_basis]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (↑(↑B.basis.repr ((fun i => B'.gen ^ ↑i) j)) i)
[PROOFSTEP]
refine' repr_pow_isIntegral hB (fun i => _) hmin _ _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr B'.gen) i)
[PROOFSTEP]
rw [← h, aeval_eq_sum_range, LinearEquiv.map_sum, Finset.sum_apply']
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R (Finset.sum (Finset.range (natDegree P + 1)) fun k => ↑(↑B.basis.repr (coeff P k • B.gen ^ k)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun n _ => _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (natDegree P + 1)
⊢ IsIntegral R (↑(↑B.basis.repr (coeff P n • B.gen ^ n)) i)
[PROOFSTEP]
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, LinearEquiv.map_smul, algebraMap_smul]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (natDegree P + 1)
⊢ IsIntegral R (↑(coeff P n • ↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
exact isIntegral_smul _ (repr_gen_pow_isIntegral hB hmin _ _)
