R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p, p > 0 ∧ MixedCharZero R p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ IsEmpty (Algebra ℚ R) ↔ ∃ p, p > 0 ∧ MixedCharZero R p
rw [← not_iff_not]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p, p > 0 ∧ MixedCharZero R p
push_neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
rw [not_isEmpty_iff, ← EqualCharZero.iff_not_mixedCharZero]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
apply EqualCharZero.nonempty_algebraRat_iff