[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] A revision
Hi:
I am asking it here rather than at the developer-forum as it might be
of a general interest.
I am finishing the proof of the finite skew-field Weddernburn theorem
and I need to use stuff from POLYNOM4 and POLYNOM5 on univariate
polynomials. Robert Milewski has proven some facts that I need
requiring that the coefficients are from a Field-like structure where
domRing (integral domain) would suffice. Shall I continue using
Field-like, or revise POLYNOM4 and POLYNOM5, or maybe steal Robert's theorems
and generalize them?
I guess that the revision of the past is the way to go. I am sure
that if the MML submissions were reviewed before inclusion then many
such issues would have been caught early and thus there would be no
need for some revisions of the past.
The question is: will we have some reviewing for MML any time soon?
Cheers,
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr