-
Notifications
You must be signed in to change notification settings - Fork 318
/
Conjneg.lean
38 lines (27 loc) · 1.1 KB
/
Conjneg.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
/-
Copyright (c) 2024 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Algebra.Order.Pi
import Mathlib.Algebra.Order.Star.Basic
import Mathlib.Algebra.Star.Conjneg
/-!
# Order properties of conjugation-negation
-/
open scoped ComplexConjugate
variable {ι G R : Type*} [AddGroup G]
section OrderedCommSemiring
variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f : G → R}
@[simp] lemma conjneg_nonneg : 0 ≤ conjneg f ↔ 0 ≤ f :=
(Equiv.neg _).forall_congr' <| by simp [starRingEnd_apply]
@[simp] lemma conjneg_pos : 0 < conjneg f ↔ 0 < f := by
simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]
end OrderedCommSemiring
section OrderedCommRing
variable [OrderedCommRing R] [StarRing R] [StarOrderedRing R] {f : G → R}
@[simp] lemma conjneg_nonpos : conjneg f ≤ 0 ↔ f ≤ 0 := by
simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]
@[simp] lemma conjneg_neg' : conjneg f < 0 ↔ f < 0 := by
simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]
end OrderedCommRing