English
If r ∈ S, for all x,y in LocalizedModule S M, r • x = y if and only if x equals (Localization.mk 1 ⟨r, hr⟩) • y, reflecting a precise cancellation when r comes from the localization set.
Русский
Если r ∈ S, для любых x,y в LocalizedModule S M верно, что r • x = y тогда и только тогда, когда x = (Localization.mk 1 ⟨r, hr⟩) • y, отражая точную отмену, когда r принадлежит локализационной множеству.
LaTeX
$$$r \\cdot x = y \\;\\Leftrightarrow\\; x = \\mathrm{Localization.mk}(1,\\langle r, hr \\rangle) \\cdot y$$$
Lean4
theorem smul_eq_iff_of_mem (r : R) (hr : r ∈ S) (x y : LocalizedModule S M) :
r • x = y ↔ x = Localization.mk 1 ⟨r, hr⟩ • y := by
induction x using induction_on with
| h m s =>
induction y using induction_on with
| h n t =>
rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]
simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
fconstructor
· rintro ⟨a, ha, eq1⟩
refine ⟨a, ha, ?_⟩
rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
· rintro ⟨a, ha, eq1⟩
refine ⟨a, ha, ?_⟩
rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]
