case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 0 * (r /ₒ s) = 0
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization R S
⊢ 0 * x = 0
induction' x using OreLocalization.ind with r s
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 0 * r /ₒ (s * 1) = 0 /ₒ 1
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 0 * (r /ₒ s) = 0
rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s r 1 (by simp)]
no goals
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 0 * r /ₒ (s * 1) = 0 /ₒ 1
simp
no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ r * ↑1 = ↑1 * r
simp