Hi Manuel,
On 27/06/15 09:06, Florian Haftmann wrote:
What about: »a = unit_factor a * normalize a«
Sounds reasonable.
See now cb21b7022b00 ff.
After accepting that gcd must always target a normalized segment of the
underlying ring structure, it is quite obvious how the abstract
As for the terminology, I think I did not find this concept in the
literature and just invented names that seemed reasonable to me at the
time. I agree that normalization_factor perhaps gives the wrong idea; if
you want to change it to something else, I have no objections, but I do
think
On 27/06/15 09:06, Florian Haftmann wrote:
What about: »a = unit_factor a * normalize a«
Sounds reasonable.
I still had the hope that it would be possible to develop an abstract
specification for gcd which would form a lattice: »gcd a a = a«. But
now I cam to realize that for Gcd :: 'a set =
Hallo,
thanks for all the good work. It's nice to finally see my work
integrated so neatly into HOL.
1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on
