case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : { x // x ∈ S }
⊢ 0 • mk m s = 0
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
⊢ 0 • x = 0
induction' x using LocalizedModule.induction_on with m s
no goals
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : { x // x ∈ S }
⊢ 0 • mk m s = 0
rw [← Localization.mk_zero s, mk_smul_mk, zero_smul, zero_mk]