chore(Algebra/DirectSum/Ring): add missing rfl lemma (#7575)

This isn't a simp lemma for the same reason that `Algebra.TensorProduct.one_def` isn't. Also simplifies the term in the instance.
leanprover-community · Oct 9, 2023 · 1d33c1b · 1d33c1b
1 parent 196e587
commit 1d33c1b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Mathlib/Algebra/DirectSum/Ring.lean b/Mathlib/Algebra/DirectSum/Ring.lean
@@ -158,7 +158,9 @@ section One
 
 variable [Zero ι] [GradedMonoid.GOne A] [∀ i, AddCommMonoid (A i)]
 
-instance : One (⨁ i, A i) where one := DirectSum.of (fun i => A i) 0 GradedMonoid.GOne.one
+instance : One (⨁ i, A i) where one := DirectSum.of A 0 GradedMonoid.GOne.one
+
+theorem one_def : 1 = DirectSum.of A 0 GradedMonoid.GOne.one := rfl
 
 end One