mk'_neg — Mathlib

English

mk m s equals the mk' of the linear map with the same data: LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s.

Русский

mk m s эквивалентно mk' линейного отображения: LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s.

LaTeX

$$$\\mathrm{LocalizedModule.mk} \\, m \\, s = mk' (\\mathrm{LocalizedModule.mkLinearMap} \\, S \\, M) \\, m \\, s$$$

Lean4

theorem mk'_neg {M M' : Type*} [AddCommGroup M] [SubtractionCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M')
    [IsLocalizedModule S f] (m : M) (s : S) : mk' f (-m) s = -mk' f m s :=
  by
  delta mk'
  rw [LocalizedModule.mk_neg, map_neg]

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