R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
⊢ integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
refine' Polynomial.ext_iff.trans (Polynomial.ext_iff.trans _).symm
case intro.mk
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
obtain ⟨⟨b, nonzero⟩, hb⟩ := integerNormalization_spec (nonZeroDivisors A) p
case intro.mk.mp
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff p n = coeff 0 n
i : ℕ
⊢ coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i

case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
⊢ coeff p i = coeff 0 i
case intro.mk
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
constructor <;> intro h i
no goals
case intro.mk.mp
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff p n = coeff 0 n
i : ℕ
⊢ coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i
rw [coeff_zero, ← to_map_eq_zero_iff (K := K), hb i, h i, coeff_zero, smul_zero]
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i
⊢ coeff p i = coeff 0 i
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
⊢ coeff p i = coeff 0 i
have hi := h i
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ coeff p i = coeff 0 i
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i
⊢ coeff p i = coeff 0 i
rw [Polynomial.coeff_zero, ← @to_map_eq_zero_iff A _ K, hb i, Algebra.smul_def] at hi
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ ¬↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ coeff p i = coeff 0 i
apply Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hi)
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ False
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ ¬↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
intro h
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ b = 0
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ False
apply mem_nonZeroDivisors_iff_ne_zero.mp nonzero
no goals
case intro.mk.mpr
R : Type ?u.88248
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.88455
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.88711
inst✝⁶ : CommRing P
A : Type u_2
K : Type u_1
C : Type ?u.88723
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ b = 0
exact to_map_eq_zero_iff.mp h