Cleanup some phantom related stuff and proofs

math-comp / multinomials

Multinomials for the Mathematical Components library.

Other

14 stars 12 forks source link

Cleanup some phantom related stuff and proofs #84

Closed pi8027 closed 11 months ago

pi8027 commented 11 months ago

Extracted from #83

This PR:

deprecates the notations [mmorphism of f (as g)] and [measure of f] (but keeps {cmonom I}, {fmonom I}, {mpoly T [n]}, and [mpoly D]),
changes the statement of malgP, and
fixes the notation scopes of the arguments of mcoeff and mkmalgU to avoid writing them explicitly, e.g., in the statement of malgME.

pi8027 commented 11 months ago

I plan to self-merge this PR by the end of today (mainly because we will discuss #83 tomorrow). It would be nice if someone could take a brief look at this PR before that (just to make sure that I'm not doing a stupid thing).