How to write a polynomial?

Stream: mathlib4

[Christopher Hoskin]

There seem to be two ways one could write a polynomial in Mathlib:

import Mathlib.Algebra.Polynomial.Basic

variable {R : Type*} [Semiring R] {a b c : R}

open Polynomial

#check (a • X ^ 2 + b • X + C c : R[X])

#check (C a * X ^ 2 + C b * X + C c : R[X])

The former seems more natural to me, but the latter seems to be the preferred form, is that correct? Presumably this is to emphasise R[X] as a ring rather than a module?

(PR which prompted this question: #25905)

Thanks,

Christopher

[Michael Stoll]

The first version would be more consistent as a • X ^ 2 + b • X + c • 1.

One could also replace a • _ by agebraMap R R[X] a * _ ...

[Michael Stoll]

But I agree that it would be nice to have an agreed-upon (simp?) normal form that facilitates manipulating polynomials.

[Edward van de Meent]

for tactic reasons i'd like to argue for the smul version, as i think that the module tactic works on that form?

[Edward van de Meent]

i might be wrong about that though

[Kenny Lau]

I thought we don't have a good tactic for polynomials as of now

[Notification Bot]

29 messages were moved from this topic to #mathlib4 > Tactic for polynomial/algebra by Kenny Lau.

[Violeta Hernández]

I tried to use the smul form not too long ago, only to quickly realize the lack of API around it, and that most results expected the mul form instead...

[Eric Wieser]

I think it's clear that if we switched we'd have to do so globally across the polynomial API