-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer #2416
Comments
It is even worse. |
Changing
As to |
Yes, we should fix this in 3.0 |
Currently I use
|
Cf #679 #2115 (and perhaps others, incl. #1578 ), so marking this as |
It is better to use above the names Irreducible-adHoc and Prime-adHoc with using |
Yes, okay closing as duplicate. Please feel free to continue the discussion in #2115 |
lib-2.1-rc1 has general definitions for
Irreducible, Prime
for Magma, CancellativeCommutativeSemiring,and also some proofs for them (see Algebra/Definitions/ and certain other places).
And
ℕ, ℤ
do have their instances *-magma, cancellativeCommutativeSemiring.So, it has sense for
ℕ
andℤ
to import the general definitions ofIrreducible, Prime
as specialization(by substituting the module parameters) and to use them instead of declaring ad-hoc definitions by new. For example, the parts of
Nat.Primality.Prime
can be derived from the general definition ofPrime
.If the ad-hoc local definitions occur useful, it would have sense to rename them and to hide them under
private
.The matter is that the general definitions and many their related properties work not only for
ℕ
, but also forℤ
and for polynomials overℤ
and for many other domains.For example, I use
Nat.Factorization.factorise
, but I need to convert the parts ofPrimeFactorisation
to general ones,say, to convert
factorsPrime
from the ad-hoc definitionPrime
to generalPrime
, and so on.Such renaming and conversion complicates the code.
The text was updated successfully, but these errors were encountered: