[isabelle-dev] type class ordered_semiring_1

[Lawrence Paulson]

So this not only works but has been installed.

But why zero_neq_one rather than zero_less_one? Are there really ordered semirings where 0<1 does not hold? Other AFP entries use that version.

Larry

> On 23 Apr 2025, at 18:16, Florian Haftmann <florian.haftmann at cit.tum.de> wrote:
> 
> 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.
>