K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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)
intro i
K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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)
let Q := X ^ n %ₘ minpoly R B.gen
K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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)
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
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)

case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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)
by_cases hQ : Q = 0
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
rw [this, aeval_eq_sum_range' hlt]
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
simp only [LinearEquiv.map_sum, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finset.sum_apply']
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
refine' IsIntegral.sum _ fun j hj => _
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
replace hj := Finset.mem_range.1 hj
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
  Algebra.smul_def, LinearEquiv.map_smul]
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)

case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
by_cases hij : (⟨j, hj⟩ : Fin _) = i
K : Type ?u.78093
S : Type u_1
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_2
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
K : Type ?u.78093
S : Type u_1
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_2
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
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
no goals
K : Type ?u.78093
S : Type u_1
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_2
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
simp
no goals
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)
simp [this, hQ, isIntegral_zero]
K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
  natDegree_lt_natDegree_iff hQ]
K : Type ?u.78093
S : Type u_1
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_2
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)
K : Type ?u.78093
S : Type u_1
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_2
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)
letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
no goals
K : Type ?u.78093
S : Type u_1
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_2
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)
exact degree_modByMonic_lt _ (minpoly.monic hB)
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)
simp only [hij, eq_self_iff_true, if_true]
case pos
K : Type ?u.78093
S : Type u_1
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_2
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))
case pos
K : Type ?u.78093
S : Type u_1
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_2
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)
rw [Algebra.smul_def, mul_one]
no goals
case pos
K : Type ?u.78093
S : Type u_1
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_2
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))
exact isIntegral_algebraMap
no goals
case neg
K : Type ?u.78093
S : Type u_1
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_2
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)
simp [hij, isIntegral_zero]