[isabelle-dev] type class ordered_semiring_1

[Florian Haftmann]

Reving this old thread after 
https://isabelle.sketis.net/repos/afp-devel/rev/a194ec58339d the 
situation is now:

In Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy, type class 
ordered_semiring_1 is now also based on zero_neq_one

Hence it should now be equivalent to its counterpart 
LLL_Basis_Reduction/Missing_Lemmas.thy

And note that there is also Jordan_Normal_Form/Missing_Ring.thy with 
similar type classes.

I do not know if anybody has an agenda to unify these; a suitable 
starting point could to be to integrate (parts of) 
Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy into 
HOL-Library.Ordered_Rings_and_Fields and then consolidate with the two 
other theories.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250423/96b1d985/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250423/96b1d985/attachment.sig>