units — Mathlib

English

If M, M2 are modules with a compatible SMul structure over ℤ and S, then the same structure extends to M and M2 with units of a ring.

Русский

Если существуют согласованные скаляры над ℤ и S на модулях M и M2, то такая же структура распространяется на M и M2 через юниты кольца.

LaTeX

$$$\text{CompatibleSMul } M M_2 \mathbb{Z} S$$$

Lean4

instance units {R S : Type*} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂]
    [CompatibleSMul M M₂ R S] : CompatibleSMul M M₂ Rˣ S :=
  ⟨fun fₗ c x ↦ (CompatibleSMul.map_smul fₗ (c : R) x :)⟩

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