docs: fix typo (#12659)

`single 1 1` is the `MonoidAlgebra` unit, while the `AddMonoidAlgebra` unit is `single 0 1`.
leanprover-community · May 4, 2024 · b632537 · b632537
1 parent a4b23a6
commit b632537
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
@@ -1358,7 +1358,7 @@ section One
 
 variable [Semiring k] [Zero G] [NonAssocSemiring R]
 
-/-- The unit of the multiplication is `single 1 1`, i.e. the function
+/-- The unit of the multiplication is `single 0 1`, i.e. the function
   that is `1` at `0` and zero elsewhere. -/
 instance one : One k[G] :=
   ⟨single 0 1⟩