Theorems · Theorem · ring theory

DirectSum.of_eq_of_gradedMonoid_eq

∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : (i : ι) → AddCommMonoid (A i)] {i j : ι} {a : A i}
  {b : A j}, GradedMonoid.mk i a = GradedMonoid.mk j b → (DirectSum.of A i) a = (DirectSum.of A j) b

Defined in

Mathlib.Algebra.DirectSum.Ring

Cited by

8 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddCommMonoid