English
Singleton finsupp maps to the corresponding lof injection under finsuppLEquivDirectSum.
Русский
Одиночный finsupp отображается в соответствующее вложение lof через эквиваленцию.
LaTeX
$$$finsuppLEquivDirectSum\, R\, M\, ι\,(Finsupp.single\ i\ m) = DirectSum.lof\, R\, ι\, (\lambda j, M)\, i\ m$$
Lean4
/-- Build a `DirectSum.GSemiring` instance for a collection of additive submonoids. -/
instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
[SetLike.GradedMonoid A] : DirectSum.GSemiring fun i => A i :=
{ SetLike.gMonoid A with
mul_zero := fun _ => Subtype.ext (mul_zero _)
zero_mul := fun _ => Subtype.ext (zero_mul _)
mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
add_mul := fun _ _ _ => Subtype.ext (add_mul _ _ _)
natCast := fun n => ⟨n, SetLike.natCast_mem_graded _ _⟩
natCast_zero := Subtype.ext Nat.cast_zero
natCast_succ := fun n => Subtype.ext (Nat.cast_succ n) }
