instIsScalarTowerHahnSeries_1 — Mathlib

English

The scalar actions satisfy the tower identity for all engaging objects.

Русский

Свойство башни скаляров выполняется для всех задействованных объектов.

LaTeX

$$$\text{IsScalarTower } R\ (\mathrm{HahnSeries}\; \Gamma\; R)\ (\mathrm{HahnModule}\; \Gamma'\; R\ V)$$$

Lean4

instance [Semiring R] [Module R V] : IsScalarTower R (HahnSeries Γ R) (HahnModule Γ' R V) where
  smul_assoc r x a := by rw [← HahnSeries.single_zero_mul_eq_smul, mul_smul', ← single_zero_smul_eq_smul Γ]

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