Re: [isabelle] Gcd and algebraic structures



[…]

Even more thoughts.

1) A characterisation of a factorial ring.

May sth. like this:

> class factorial_(semi)ring = (sem)idom +
>   fixes is_prime :: "α ⇒ bool"
>   assumes "(⋀a. a dvd p ⟹ a dvd 1 ∨ p dvd a) ⟹ is_prime p
>   assumes "is_prime p ⟹ a dvd p ⟹ a dvd 1 ∨ p dvd a"
>   assumes "(⋀a b. p dvd a * b ⟹ p dvd a ∨ p dvd b) ⟹ is_prime p
>   assumes "is_prime p ⟹ p dvd a * b ⟹ p dvd a ∨ p dvd b"

2)

> Maybe any (semi)ring_gcd is also a factorial_(semi)ring?
> 
> The direction <-- is obvious.  For --> I am uncertain.
> http://en.wikipedia.org/wiki/Greatest_common_divisor (section »The gcd
> in commutative rings«) suggests that it does not hold in general.

Maybe --> holds since the given specification for (semi)ring_gcd demands
that every two elements have a gcd.  From this it might follow that
unique factors can be carved out using iterative gcd computations (I
have once seen such a proof for the natural numbers, but I don't know
whether this generalizes).

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.