instBaseSMul — Mathlib

English

The extensionality principle for HahnModule: equality is determined by coefficients after mapping back via of.

Русский

Принцип экстенсиональности для HahnModule: равенство определяется по коэффициентам после отображения обратно через of.

LaTeX

$$$\forall x,y, ((\mathrm{of} R)^{-1} x).\mathrm{coeff} = ((\mathrm{of} R)^{-1} y).\mathrm{coeff} \Rightarrow x = y$$$

Lean4

instance instBaseSMul {V} [Monoid R] [AddMonoid V] [DistribMulAction R V] : SMul R (HahnModule Γ R V) :=
  inferInstanceAs <| SMul R (HahnSeries Γ V)

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