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.

source

@[protected, instance]

def rat.star_ring :

star_ring ℚ

Equations

rat.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := id ℚ}, star_involutive := rat.star_ring._proof_1}, star_mul := rat.star_ring._proof_2}, star_add := rat.star_ring._proof_3}

source

@[protected, instance]

def rat.has_trivial_star :

has_trivial_star ℚ

source

@[protected, instance]

def rat.star_ordered_ring :

star_ordered_ring ℚ

Equations

rat.star_ordered_ring = star_ordered_ring.of_nonneg_iff rat.star_ordered_ring._proof_1 rat.star_ordered_ring._proof_2