instSMul — Mathlib

English

There is a scalar action of HahnSeries Γ R on HahnModule Γ' R V, i.e., a well-defined SMul between these structures.

Русский

Существует скалярное действие ряда Хана на модуль Хана: задано допустимое скалярное умножение между этими структурами.

LaTeX

$$$\text{SMul}\,(\HahnSeries\,\Gamma\,R)\, (\HahnModule\,\Gamma'\,R\,V)$$$

Lean4

instance instSMul : SMul (HahnSeries Γ R) (HahnModule Γ' R V) where
  smul x
    y :=
    (of R)
      { coeff := fun a =>
          ∑ ij ∈ VAddAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
            x.coeff ij.fst • ((of R).symm y).coeff ij.snd
        isPWO_support' :=
          haveI h :
            {a : Γ' |
                (∑ ij ∈ VAddAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
                    x.coeff ij.fst • ((of R).symm y).coeff ij.snd) ≠
                  0} ⊆
              {a : Γ' | (VAddAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a).Nonempty} :=
            by
            intro a ha
            contrapose! ha
            simp [not_nonempty_iff_eq_empty.1 ha]
          isPWO_support_vaddAntidiagonal.mono h }

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