instModule — Mathlib

English

The product of two well-founded support unions is itself well-founded under multiplication.

Русский

Произведение двух хорошо упорядоченных опор сохраняет свойство IsPWO под умножением.

LaTeX

$$$ isPWO_iUnion\_support\_prod\_mul \; hs ht : (\bigcup i, (s i).support) \cup (\bigcup j, (t j).support).IsPWO $$$

Lean4

instance [AddCommMonoid V] [Module R V] : Module (HahnSeries Γ R) (SummableFamily Γ' V α)
    where
  smul := (· • ·)
  smul_zero _ := ext fun _ => by simp
  zero_smul _ := ext fun _ => by simp
  one_smul _ := ext fun _ => by rw [smul_apply, HahnModule.one_smul', Equiv.symm_apply_apply]
  add_smul _ _ _ := ext fun _ => by simp [add_smul]
  smul_add _ _ _ := ext fun _ => by simp
  mul_smul _ _ _ := ext fun _ => by simp [HahnModule.instModule.mul_smul]

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