R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
⊢ ↑I * (↑I)⁻¹ = 1
apply mul_inv_cancel_of_le_one hI0
case pos
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1

case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
by_cases hJ0 : I * (I : FractionalIdeal A⁰ K)⁻¹  = 0
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ x ∈ (fun a => ↑a) 1
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
intro x hx
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ x ∈ integralClosure A K
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ x ∈ (fun a => ↑a) 1
suffices x ∈ integralClosure A K by
  rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
    ← mem_one_iff] at this
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ ∃ M, Submodule.FG (↑Subalgebra.toSubmodule M) ∧ x ∈ M
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ x ∈ integralClosure A K
rw [mem_integralClosure_iff_mem_FG]
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
y : K
hy : y ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ y ∈ ↑(↑I)⁻¹
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
⊢ ∃ M, Submodule.FG (↑Subalgebra.toSubmodule M) ∧ x ∈ M
refine ⟨AlgHom.range (Polynomial.aeval x : A[X] →ₐ[A] K),
  isNoetherian_submodule.mp (isNoetherian (I : FractionalIdeal A⁰ K)⁻¹) _ fun y hy => ?_,
  ⟨Polynomial.X, Polynomial.aeval_X x⟩⟩
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ ↑(Polynomial.aeval x) p ∈ ↑(↑I)⁻¹
case neg
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
y : K
hy : y ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ y ∈ ↑(↑I)⁻¹
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp hy
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ (Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun i => Polynomial.coeff p i • x ^ i) ∈ ↑(↑I)⁻¹
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ ↑(Polynomial.aeval x) p ∈ ↑(↑I)⁻¹
rw [Polynomial.aeval_eq_sum_range]
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
hi : i ∈ Finset.range (Polynomial.natDegree p + 1)
⊢ x ^ i ∈ ↑(↑I)⁻¹
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ (Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun i => Polynomial.coeff p i • x ^ i) ∈ ↑(↑I)⁻¹
refine Submodule.sum_mem _ fun i hi => Submodule.smul_mem _ _ ?_
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
⊢ x ^ i ∈ ↑(↑I)⁻¹
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
hi : i ∈ Finset.range (Polynomial.natDegree p + 1)
⊢ x ^ i ∈ ↑(↑I)⁻¹
clear hi
case neg.intro.zero
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ x ^ Nat.zero ∈ ↑(↑I)⁻¹

case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x ^ Nat.succ i ∈ ↑(↑I)⁻¹
case neg.intro
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
⊢ x ^ i ∈ ↑(↑I)⁻¹
induction' i with i ih
case pos
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ 0 ≤ 1
case pos
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
rw [hJ0, inv_zero']
no goals
case pos
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ 0 ≤ 1
exact zero_le _
no goals
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
this : x ∈ integralClosure A K
⊢ x ∈ (fun a => ↑a) 1
rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
  ← mem_one_iff] at this
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ x * b ∈ (↑I)⁻¹
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
⊢ ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
intro b hb
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ x * b ∈ (↑I)⁻¹
rw [mem_inv_iff]
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ ↑(↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
dsimp only at hx
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ ≠ 0

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ ↑(↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
rw [val_eq_coe, mem_coe, mem_inv_iff] at hx
case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ ≠ 0

R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ ≠ 0

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
swap
case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0

R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1

case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
swap
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * (y * b) ∈ 1
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * b * y ∈ 1
simp only [mul_assoc, mul_comm b] at hx ⊢
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
y : K
hy : y ∈ ↑I
⊢ x * (y * b) ∈ 1
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ (y : K), y ∈ ↑I → x * (y * b) ∈ 1
intro y hy
no goals
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : ∀ (y : K), y ∈ ↑I * (↑I)⁻¹ → x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
y : K
hy : y ∈ ↑I
⊢ x * (y * b) ∈ 1
exact hx _ (mul_mem_mul hy hb)
no goals
case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ ≠ 0
exact hJ0
no goals
case hI
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ↑I ≠ 0
exact coeIdeal_ne_zero.mpr hI0
case neg.intro.zero
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ 1 ∈ ↑(↑I)⁻¹
case neg.intro.zero
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ x ^ Nat.zero ∈ ↑(↑I)⁻¹
rw [pow_zero]
no goals
case neg.intro.zero
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
⊢ 1 ∈ ↑(↑I)⁻¹
exact one_mem_inv_coe_ideal hI0
case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x ^ Nat.succ i ∈ (↑I)⁻¹
case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x ^ Nat.succ i ∈ ↑(↑I)⁻¹
show x ^ i.succ ∈ (I⁻¹ : FractionalIdeal A⁰ K)
case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x * x ^ i ∈ (↑I)⁻¹
case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x ^ Nat.succ i ∈ (↑I)⁻¹
rw [pow_succ]
no goals
case neg.intro.succ
R : Type ?u.444206
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ (b : K), b ∈ (↑I)⁻¹ → x * b ∈ (↑I)⁻¹
p : A[X]
hy : ↑(Polynomial.aeval x) p ∈ ↑Subalgebra.toSubmodule (AlgHom.range (Polynomial.aeval x))
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x * x ^ i ∈ (↑I)⁻¹
exact x_mul_mem _ ih