lsmul_apply_apply — Mathlib

English

For any s ∈ S and x ∈ RestrictScalars R S M, the lsmul action agrees with the corresponding action transported by addEquiv: lsmul(s)(x) = (addEquiv)^{-1}( s • addEquiv(x) ).

Русский

Для любого s ∈ S и x ∈ RestrictScalars R S M скалярное действие lsmul совпадает с соответствующим действием, переносимым через addEquiv: lsmul(s)(x) = (addEquiv)^{-1}( s • addEquiv(x) ).

LaTeX

$$$\mathrm{RestrictScalars.lsmul}_{R,S,M} \, s \, x = (\mathrm{addEquiv}_{R,S,M})^{-1} \bigl( s \cdot \mathrm{addEquiv}_{R,S,M} x \bigr)$$$

Lean4

theorem lsmul_apply_apply (s : S) (x : RestrictScalars R S M) :
    RestrictScalars.lsmul R S M s x = (RestrictScalars.addEquiv R S M).symm (s • RestrictScalars.addEquiv R S M x) :=
  rfl

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