`Factorization` and `factor`

[mechvel]

This is about lib-2.3 and Data.Nat.Primality.Factorisation.

It is more classical to (1) call it Factorization - with z instead of s (2) record PrimeFactorisation --> record Factorization (factorization is always to primes, and again z), (3) factorise --> factor.

For example, see these names in the "Axiom" book by Jenks and Sutor. I believe the same it is in textbooks on computer algebra.

Another (great) point remains that it is desirable to replace the ad hoc definitions of GCD and Factorization with the general definitions with introducing their instances for Nat and Integer.

The DoCon-A library release candidate 3.2-rc4 includes such a treating of GCD and Factorization: http://www.botik.ru/pub/local/Mechveliani/docon-A/ (GCDSemiring, GCDDomain, FactorizationSemiring, UFD ...).

[Taneb]

It is more classical to (1) call it Factorization - with z instead of s

This is a difference between US spelling (with the z) and UK/Commonwealth spelling (with the s). As most of the regular contributors to this library are either in or from Commonwealth countries (UK, Australia, Canada) we went with the "s" spelling.

(2) record PrimeFactorisation --> record Factorization (factorization is always to primes, and again z),

It is not true that factorisation is always to primes, only into factors (~ divisors). For example, a valid factorisation of 24 could be 4 times 6, even though both factors there are composite.

(3) factorise --> factor

Both terms are used. I don't feel that strongly about what we call it, but I don't think we should change it without a good reason.

Another (great) point remains that it is desirable to replace the ad hoc definitions of GCD and Factorization with the general definitions with introducing their instances for Nat and Integer.

The DoCon-A library release candidate 3.2-rc4 includes such a treating of GCD and Factorization: http://www.botik.ru/pub/local/Mechveliani/docon-A/ (GCDSemiring, GCDDomain, FactorizationSemiring, UFD ...).

A lot of number theory works with specifically the integers and the naturals, without generalizing to more abstract structures. Maybe we will do something in this direction in the future, if someone interested takes it up, but what we have now works perfectly well for what it is.

[mechvel]

It is not true that factorisation is always to primes, only into factors (~ divisors). For example, a valid factorisation of 24 could be 4 times 6, even though both factors there are composite.

I meant that factor usually means by default factoring to primes, while other kinds of factoring are named with adding some word, say, factorToSquareFree, factorToSmallers (contrived examples).
But I would not say that this is greatly important.

A lot of number theory works with specifically the integers and the naturals, without generalizing to more abstract structures.

Standard library for Agda is not only for the number theory, rather it is natural for it to implement a generic approach.