We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9944fe2 commit bfefa91Copy full SHA for bfefa91
1 file changed
Mathlib/Algebra/MonoidAlgebra/Defs.lean
@@ -468,9 +468,12 @@ instance one : One R[M] where one := single 1 1
468
@[to_additive (dont_translate := R) one_def]
469
lemma one_def : (1 : R[M]) = single 1 1 := rfl
470
471
-@[to_additive (attr := simp) (dont_translate := R)]
+@[to_additive (attr := simp) (dont_translate := R) coeff_one_zero]
472
lemma coeff_one_one : (1 : R[M]).coeff 1 = 1 := by simp [one_def]
473
474
+@[deprecated (since := "2026-07-15")]
475
+alias _root_.AddMonoidAlgebra.coeff_zero_zero := AddMonoidAlgebra.coeff_one_zero
476
+
477
end One
478
479
section Mul
0 commit comments