R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
s : { x // x ∈ S }
⊢ ∃ u v, 0 * ↑u = 0 * v ∧ ↑1 * ↑u = ↑s * v
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
s : { x // x ∈ S }
⊢ 0 /ₒ s = 0
rw [OreLocalization.zero_def, oreDiv_eq_iff]
no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
s : { x // x ∈ S }
⊢ ∃ u v, 0 * ↑u = 0 * v ∧ ↑1 * ↑u = ↑s * v
exact ⟨s, 1, by simp⟩
no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
s : { x // x ∈ S }
⊢ 0 * ↑s = 0 * 1 ∧ ↑1 * ↑s = ↑s * 1
simp