[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
have hI := span_singleton_eq_bot.not.2 hf
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
let b' := ringBasis b (span { f }) hI
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
classical
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
let e := (b'.equiv ((span { f }).selfBasis b hI) <| Equiv.refl _).trans ((LinearEquiv.coord S S f hf).restrictScalars R)
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
dsimp only [LinearEquiv.trans_apply]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
refine b'.ext fun i => ?_
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul, Finset.sum_ite_eq',
  mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
change _ = f * _
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, Ideal.selfBasis_def]
rfl
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f)
    (↑LinearMap.det (↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)))
[PROOFSTEP]
let e := (b'.equiv ((span { f }).selfBasis b hI) <| Equiv.refl _).trans ((LinearEquiv.coord S S f hf).restrictScalars R)
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ Associated (↑(Algebra.norm R) f)
    (↑LinearMap.det (↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)))
[PROOFSTEP]
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ∀ (x : S),
    ↑(↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)) x =
      ↑(↑↑↑(Algebra.lmul R S) f) (↑e x)
[PROOFSTEP]
dsimp only [LinearEquiv.trans_apply]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ∀ (x : S),
    ↑(↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
            (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i))
        x =
      ↑(↑↑↑(Algebra.lmul R S) f)
        (↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
          (↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι)) x))
[PROOFSTEP]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ↑↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
      (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i) =
    LinearMap.comp (↑↑↑(Algebra.lmul R S) f)
      (LinearMap.comp ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι)))
[PROOFSTEP]
refine b'.ext fun i => ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ ↑(↑↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
          (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i))
      (↑b' i) =
    ↑(LinearMap.comp (↑↑↑(Algebra.lmul R S) f)
          (LinearMap.comp ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
            ↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι))))
      (↑b' i)
[PROOFSTEP]
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul, Finset.sum_ite_eq',
  mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    ↑(↑↑↑(Algebra.lmul R S) f)
      (↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) (↑(selfBasis b (span {f}) hI) (↑(Equiv.refl ι) i)))
[PROOFSTEP]
change _ = f * _
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    f * ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) (↑(selfBasis b (span {f}) hI) (↑(Equiv.refl ι) i))
[PROOFSTEP]
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, Ideal.selfBasis_def]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    smithCoeffs b (span {f}) hI (↑(Equiv.refl ι) i) • ↑(ringBasis b (span {f}) hI) (↑(Equiv.refl ι) i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ FiniteDimensional F (F[X] ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
refine PowerBasis.finiteDimensional ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ PowerBasis F (F[X] ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
refine AdjoinRoot.powerBasis ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0
[PROOFSTEP]
refine I.smithCoeffs_ne_zero b hI i
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
have h := span_singleton_eq_bot.not.2 hf
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
rw [natDegree_eq_of_degree_eq (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]
  -- finrank_quotient_eq_sum slow
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ ∑ i : ι, FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) =
    ∑ i : ι, natDegree (smithCoeffs b (span {f}) h i)
[PROOFSTEP]
congr with i
[GOAL]
case e_f.h
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
i : ι
⊢ FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = natDegree (smithCoeffs b (span {f}) h i)
[PROOFSTEP]
exact (AdjoinRoot.powerBasis <| smithCoeffs_ne_zero b _ h i).finrank
