English
Equality of idempotent expressions under idempotent construction.
Русский
Равенство идемпотентности при конструировании.
LaTeX
$$DirectSum.idempotent V i = DFinsupp.instDFunLike.coe (EquivLike.toFunLike.coe (DirectSum.decompose V) 1).val i$$
Lean4
/-- Build a `DirectSum.GRing` instance for a collection of additive subgroups. -/
instance gring [AddMonoid ι] [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :
DirectSum.GRing fun i => A i :=
{ SetLike.gsemiring A with
intCast := fun z => ⟨z, SetLike.intCast_mem_graded _ _⟩
intCast_ofNat := fun _n => Subtype.ext <| Int.cast_natCast _
intCast_negSucc_ofNat := fun n => Subtype.ext <| Int.cast_negSucc n }
