instModuleComplex — Mathlib

English

The injectivity of the coeHom map holds in the strengthened form: the AddMonoidHom induced by coeHom is injective.

Русский

Сильнее: инъективность отображения coeHom на уровне AddMonoidHom.

LaTeX

$$$$ \\text{Injective } (\\text{AddMonoidHom}.instFunLike.\\text{coe SlashInvariantForm.coeHom}). $$$$

Lean4

instance instModuleComplex [Γ.HasDetOne] {α : Type*} [Semiring α] [Module α ℂ] [IsScalarTower α ℂ ℂ] :
    Module α (SlashInvariantForm Γ k) :=
  coeHom_injective.module α _ (fun _ _ ↦ rfl)

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