instAlgebra — Mathlib

English

There is a noncomputable algebra structure on LocalizedModule S M making it an algebra over T, compatible with the isLocalization and scalar actions.

Русский

Существует неконкретная алгебраическая структура на LocalizedModule S M, делающая его алгеброй над T, совместимой с isLocalization и скалярными действиями.

LaTeX

$$$\\text{LocalizedModule}(S,M) \\in \\text{Alg}_T$$$

Lean4

noncomputable instance {A : Type*} [Semiring A] [Algebra R A] : Algebra T (LocalizedModule S A) :=
  Algebra.ofModule smul'_mul mul_smul'

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