mathlib3 documentation

data.rat.star

Star order structure on ℚ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Here we put the trivial star operation on for convenience and show that it is a star_ordered_ring. In particular, this means that every element of is a sum of squares.

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations