Documentation

Mathlib.Algebra.Order.Star.Conjneg

Order properties of conjugation-negation #

source
@[simp]
theorem conjneg_nonneg {G : Type u_1} {R : Type u_2} [AddGroup G] [CommSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {f : G → R} :
0 ≤ conjneg f ↔ 0 ≤ f
source
@[simp]
theorem conjneg_pos {G : Type u_1} {R : Type u_2} [AddGroup G] [CommSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {f : G → R} :
0 < conjneg f ↔ 0 < f
source
@[simp]
theorem conjneg_nonpos {G : Type u_1} {R : Type u_2} [AddGroup G] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {f : G → R} :
conjneg f ≤ 0 ↔ f ≤ 0
source
@[simp]
theorem conjneg_neg' {G : Type u_1} {R : Type u_2} [AddGroup G] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {f : G → R} :
conjneg f < 0 ↔ f < 0