case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ span R {a} = ⊤
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : span R {p} < I
⊢ I = ⊤
rcases principal I with ⟨a, rfl⟩
case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ IsUnit a
case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ span R {a} = ⊤
erw [Ideal.span_singleton_eq_top]
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
⊢ IsUnit a
case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ IsUnit a
rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
hb : IsUnit b
⊢ span R {a} ≤ span R {a * b}
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
⊢ IsUnit a
refine' (of_irreducible_mul hp).resolve_right (mt (fun hb => _) (not_le_of_lt hI))
no goals
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
hb : IsUnit b
⊢ span R {a} ≤ span R {a * b}
erw [Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]