isScalarTower — Mathlib

English

Transfer an IsScalarTower across an Equiv: if e: α ≃ β and M,N act on β with IsScalarTower M N β, then α inherits IsScalarTower M N α via e.

Русский

Переносим IsScalarTower через эквив: если e: α ≃ β и M,N действуют на β с IsScalarTower, то α наследует IsScalarTower через e.

LaTeX

$$$\text{Equiv.isScalarTower } M N e: IsScalarTower M N α$ given $IsScalarTower M N β$.$$

Lean4

/-- Transfer `IsScalarTower` across an `Equiv` -/
@[to_additive /-- Transfer `VAddAssocClass` across an `Equiv` -/
    ]
protected theorem isScalarTower (e : α ≃ β) [IsScalarTower M N β] :
    letI := e.smul M
    letI := e.smul N
    IsScalarTower M N α :=
  letI := e.smul M
  letI := e.smul N
  { smul_assoc := by simp [smul_def, smul_assoc] }

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