asModule — Mathlib

English

ρ.asModule is a type alias for V equipped with a module structure over MonoidAlgebra(k,G).

Русский

ρ.asModule есть псевдотип V, оснащённый модульной структурой над MonoidAlgebra(k,G).

LaTeX

$$def asModule : Representation k G V → Type := V$$

Lean4

/-- If `ρ : Representation k G V`, then `ρ.asModule` is a type synonym for `V`,
which we equip with an instance `Module (MonoidAlgebra k G) ρ.asModule`.

You should use `asModuleEquiv : ρ.asModule ≃+ V` to translate terms.
-/
@[nolint unusedArguments]
def asModule (_ : Representation k G V) :=
  V
deriving AddCommMonoid, Module k

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