[Merged by Bors] - feat(AddMonoidAlgebra*): add notation R[A] for addMonoidAlgebra R A

[adomani]

Introduce the notation R[A] for AddMonoidAlgebra R A. This is to align Mathlibs notation with the standard notation for group ring.

The notation is scoped in AddMonoidAlgebra and there is no analogous notation for MonoidAlgebra.

I only used the notation for single-character R and As and only in the range [a-zA-Z].

The extra lines are all in Mathlib/Algebra/MonoidAlgebra/Basic.lean. They are accounted for by extra text in the doc-module and the actual notation.

Affected files:

Counterexamples/ZeroDivisorsInAddMonoidAlgebras
Algebra/AlgebraicCard
Algebra/MonoidAlgebra/Basic
Algebra/MonoidAlgebra/Degree
Algebra/MonoidAlgebra/Division
Algebra/MonoidAlgebra/Grading
Algebra/MonoidAlgebra/NoZeroDivisors
Algebra/MonoidAlgebra/Support
Data/Polynomial/AlgebraMap
Data/Polynomial/Basic
Data/Polynomial/Eval
Data/Polynomial/Laurent
RingTheory/FiniteType

---

On line 105 of Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean, the notation does not work when used as a direct call to an implicit argument:

  · convert Commute.geom_sum₂_mul (α := AddMonoidAlgebra R A) _ (addOrderOf a) using 3
-- using `(α := R[A])` gives the error
/-
ambiguous, possible interpretations 
  R[A] : Type (max u_2 u_1)
  
  R[A] : Type ?u.23226
-/

[alreadydone]

It seems to me the notation is more suited for MonoidAlgebra, even though mathlib currently has a lot more about AddMonoidAlgebra than MonoidAlgebra ... Maybe we could ditch MonoidAlgebra and use AddMonoidAlgebra R (Additive A) when necessary? :) Oh I guess it's okay since it's scoped in AddMonoidAlgebra …

[adomani]

If wanted/possible, we could introduce the two notations R[A+] and R[G*] to distinguish the two, but, as you also observed, currently "additive" is more used than "multiplicative".

[adomani]

I just checked:

scoped[AddMonoidAlgebra] notation :9000 R "[" A "+]" => AddMonoidAlgebra R A
scoped[MonoidAlgebra]    notation :9000 R "[" A "*]" => MonoidAlgebra R A

variable {R A} [Semiring R] [Field A]

open AddMonoidAlgebra MonoidAlgebra
variable (f : R[A+]) (g : R[A*])
#check f  -- f : R[A+]
#check g  -- g : R[A*]

seems to work, if it is wanted.

Personally, I am not too convinced. Maybe, once we end up using MonoidAlgebras more, we may revise this.

[alreadydone]

Interesting that this works and Lean doesn't try to find (X : Type*).

I think it's probably safe to use the same notation for AddMonoidAlgebra and MonoidAlgebra, as long as they're scoped in different locales(=namespaces now?), since it's not common that we open both (and other conflicts will appear if we do). I imagine if we do any Kaplansky's conjecture stuff in mathlib we'd be using MonoidAlgebra rather than AddMonoidAlgebra (we have to make a choice to avoid duplication unless we make to_additive work), although existing works seem to use hand-rolled computable versions of group algebra.

[alreadydone]

LGTM

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style