English
For s ∈ S and p ∈ LocalizedModule S M, applying the endomorphism corresponding to s to divBy(s) p yields p; i.e., algebraMap_R(Module.End)(s)(divBy s p) = p.
Русский
Для s ∈ S и p ∈ LocalizedModule S M применение соответствующего эндоморфизма к divBy(s) p возвращает p; то есть algebraMap_R(Module.End)(s)(divBy s p) = p.
LaTeX
$$$\\operatorname{algebraMap}_R(\\operatorname{Module.End}_R(\\mathrm{LocalizedModule}(S,M)))\\; s\\; (\\mathrm{divBy}(s)\\; p) = p.$$$
Lean4
theorem divBy_mul_by (s : S) (p : LocalizedModule S M) :
divBy s (algebraMap R (Module.End R (LocalizedModule S M)) s p) = p :=
p.induction_on fun m t => by
rw [Module.algebraMap_end_apply, divBy_apply, ← algebraMap_smul (Localization S) (s : R), smul_def,
LocalizedModule.liftOn_mk, mul_assoc, ← smul_def, algebraMap_smul, smul'_mk, ← Submonoid.smul_def,
mk_cancel_common_right _ s]
