of_eq_of_gradedMonoid_eq — Mathlib

English

If GradedMonoid.mk i a = GradedMonoid.mk j b, then DirectSum.of A i a = DirectSum.of A j b.

Русский

Если GradedMonoid.mk i a = GradedMonoid.mk j b, то DirectSum.of A i a = DirectSum.of A j b.

LaTeX

$$$\text{GradedMonoid.mk } i a = \text{GradedMonoid.mk } j b\;\Rightarrow\; DirectSum.of A i a = DirectSum.of A j b$$$

Lean4

theorem of_eq_of_gradedMonoid_eq {A : ι → Type*} [∀ i : ι, AddCommMonoid (A i)] {i j : ι} {a : A i} {b : A j}
    (h : GradedMonoid.mk i a = GradedMonoid.mk j b) : DirectSum.of A i a = DirectSum.of A j b :=
  DFinsupp.single_eq_of_sigma_eq h

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