R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
intro I hI
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)
constructor
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast
intro a b h_ab
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ I = ⊤
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b
contrapose! hI
case cast_injective.refine'_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑(algebraMap ℚ R) (↑a - ↑b) ∈ I

case cast_injective.refine'_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ I = ⊤
refine' I.eq_top_of_isUnit_mem _ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) _))
no goals
case cast_injective.refine'_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0
simpa only [Ne.def, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI
no goals
case cast_injective.refine'_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑(algebraMap ℚ R) (↑a - ↑b) ∈ I
simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]