Skip to content

Commit 57a494b

Browse files
committed
docs(Algebra/MonoidAlgebra/Basic): fix order of arguments in docs (#7202)
The arguments to `AddMonoidAlgebra` were reversed with respect to normal use in the module docs. They also used `α` instead of `R`. For reference, these are the actual definitions: ```lean -- Data/MvPolynomial/Basic def MvPolynomial (σ : Type*) (R : Type*) [CommSemiring R] := AddMonoidAlgebra R (σ →₀ ℕ) -- Data/Polynomial/Basic structure Polynomial (R : Type*) [Semiring R] where ofFinsupp :: toFinsupp : AddMonoidAlgebra R ℕ ```
1 parent 1fa13fb commit 57a494b

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/Algebra/MonoidAlgebra/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ in the same way, and then define the convolution product on these.
3030
3131
When the domain is additive, this is used to define polynomials:
3232
```
33-
Polynomial α := AddMonoidAlgebra ℕ α
34-
MvPolynomial σ α := AddMonoidAlgebra (σ →₀ ℕ) α
33+
Polynomial R := AddMonoidAlgebra R ℕ
34+
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)
3535
```
3636
3737
When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

0 commit comments

Comments
 (0)