Documentation

Mathlib.Algebra.Order.Star.Conjneg

Order properties of conjugation-negation #

@[simp]
theorem conjneg_nonneg {G : Type u_1} {R : Type u_2} [AddGroup G] [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f : GR} :
@[simp]
theorem conjneg_pos {G : Type u_1} {R : Type u_2} [AddGroup G] [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f : GR} :
@[simp]
theorem conjneg_nonpos {G : Type u_1} {R : Type u_2} [AddGroup G] [OrderedCommRing R] [StarRing R] [StarOrderedRing R] {f : GR} :
@[simp]
theorem conjneg_neg' {G : Type u_1} {R : Type u_2} [AddGroup G] [OrderedCommRing R] [StarRing R] [StarOrderedRing R] {f : GR} :