English
Compatibility of gmodule congruence with direct sum components.
Русский
Совместимость конгруэнции gmodule с компонентами прямой суммы.
LaTeX
$$$$ \\mathrm{SetLike.gmodule}.congr_simp $$$$
Lean4
/-- `[SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜]` is the internal version of graded
module, the internal version can be translated into the external version `gmodule`. -/
instance gmodule : DirectSum.Gmodule (fun i => 𝓐 i) fun i => 𝓜 i :=
{
SetLike.gdistribMulAction 𝓐
𝓜 with
smul := fun x y => ⟨(x : A) • (y : M), SetLike.GradedSMul.smul_mem x.2 y.2⟩
add_smul := fun _a _a' _b => Subtype.ext <| add_smul _ _ _
zero_smul := fun _b => Subtype.ext <| zero_smul _ _ }
