instModuleOfIsScalarTower — Mathlib

English

There is an S-module structure on FreeLieAlgebra R X provided Semiring S with a compatible Module S R structure and IsScalarTower S R R.

Русский

Существeет структура модуля над S на FreeLieAlgebra R X при условии, что S — полукольцо, имеется совместимая структура модуля S над R и выполняется условие IsScalarTower S R R.

LaTeX

$$$\text{Module}_S\bigl(\mathrm{FreeLieAlgebra}_R X\bigr)$$$

Lean4

instance {S : Type*} [Semiring S] [Module S R] [IsScalarTower S R R] : Module S (FreeLieAlgebra R X) :=
  Function.Surjective.module S ⟨⟨Quot.mk (Rel R X), rfl⟩, fun _ _ => rfl⟩ Quot.mk_surjective (fun _ _ => rfl)

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