mul_by_divBy — Mathlib

English

Multiplication by s in the endomorphism ring is inverse to divBy(s): the endomorphism corresponding to s sends divBy(s) p back to p.

Русский

Умножение на s в кольце эндоморфизмов является обратным к divBy(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 mul_by_divBy (s : S) (p : LocalizedModule S M) :
    algebraMap R (Module.End R (LocalizedModule S M)) s (divBy s p) = p :=
  p.induction_on fun m t => by
    rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk, ← Submonoid.smul_def,
      mk_cancel_common_right _ s]

Похожие утверждения