R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsMaximal (radical I)
this : radical I = jacobson I
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ z * (x * y) - x * (z * y - 1) ∈ I
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsMaximal (radical I)
this : radical I = jacobson I
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ x ∈ I
rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]
no goals
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsMaximal (radical I)
this : radical I = jacobson I
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ z * (x * y) - x * (z * y - 1) ∈ I
exact I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz)