isScalarTower_self — Mathlib

English

If the base ring k is used to act on SkewMonoidAlgebra k G in a way compatible with the k-module structure, then SkewMonoidAlgebra k G forms a scalar tower over k with itself.

Русский

Если база кольца k действует на SkewMonoidAlgebra k G согласованно с структурой k-модуля, то SkewMonoidAlgebra k G образует скалярную башню над k самим собой.

LaTeX

$$$IsScalarTower\ k\ (SkewMonoidAlgebra\ k\ G)\ (SkewMonoidAlgebra\ k\ G)$$$

Lean4

instance isScalarTower_self [IsScalarTower k k k] : IsScalarTower k (SkewMonoidAlgebra k G) (SkewMonoidAlgebra k G) :=
  ⟨fun t a b ↦ by
    classical
    simp only [smul_eq_mul]
    refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
      simp only [← smul_sum, smul_mul_assoc, ← smul_single, zero_mul, imp_true_iff, sum_zero, single_zero];
    rfl⟩

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