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"


> Maybe any (semi)ring_gcd is also a factorial_(semi)ring?
> The direction <-- is obvious.  For --> I am uncertain.
> (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).



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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