R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ ∃ u, u • s • s • m = u • (s * s) • m
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ mk m s + 0 = mk m s
rw [← zero_mk s, mk_add_mk, smul_zero, add_zero, mk_eq]
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ ∃ u, u • s • s • m = u • (s * s) • m
exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ 1 • s • s • m = 1 • (s * s) • m
rw [one_smul, mul_smul, one_smul]