Loogle!

Result

Found 278 declarations mentioning SignType. Of these, only the first 200 are shown.

• SignType 📋 Mathlib.Basic.Sign.Defs
  : Type
• SignType.neg 📋 Mathlib.Basic.Sign.Defs
  : SignType
• SignType.pos 📋 Mathlib.Basic.Sign.Defs
  : SignType
• SignType.zero 📋 Mathlib.Basic.Sign.Defs
  : SignType
• instDecidableEqSignType 📋 Mathlib.Basic.Sign.Defs
  : DecidableEq SignType
• instFintypeSignType 📋 Mathlib.Basic.Sign.Defs
  : Fintype SignType
• instInhabitedSignType 📋 Mathlib.Basic.Sign.Defs
  : Inhabited SignType
• SignType.instCommGroupWithZero 📋 Mathlib.Basic.Sign.Defs
  : CommGroupWithZero SignType
• SignType.instLE 📋 Mathlib.Basic.Sign.Defs
  : LE SignType
• SignType.instLinearOrder 📋 Mathlib.Basic.Sign.Defs
  : LinearOrder SignType
• SignType.instMul 📋 Mathlib.Basic.Sign.Defs
  : Mul SignType
• SignType.instNeg 📋 Mathlib.Basic.Sign.Defs
  : Neg SignType
• SignType.instOne 📋 Mathlib.Basic.Sign.Defs
  : One SignType
• SignType.instZero 📋 Mathlib.Basic.Sign.Defs
  : Zero SignType
• SignType.LE 📋 Mathlib.Basic.Sign.Defs
  : SignType → SignType → Prop
• SignType.instBoundedOrder 📋 Mathlib.Basic.Sign.Defs
  : BoundedOrder SignType
• SignType.instDecidableLE 📋 Mathlib.Basic.Sign.Defs
  : DecidableLE SignType
• SignType.instHasDistribNeg 📋 Mathlib.Basic.Sign.Defs
  : HasDistribNeg SignType
• SignType.LE.of_neg 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : SignType.neg.LE a
• SignType.LE.of_pos 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : a.LE SignType.pos
• SignType.cast 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] : SignType → α
• SignType.pos_eq_one 📋 Mathlib.Basic.Sign.Defs
  : SignType.pos = 1
• SignType.zero_eq_zero 📋 Mathlib.Basic.Sign.Defs
  : SignType.zero = 0
• SignType.le_one 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : a ≤ 1
• SignType.instCoeDep 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] (s : SignType) : CoeDep SignType s α
• SignType.neg_eq_neg_one 📋 Mathlib.Basic.Sign.Defs
  : SignType.neg = -1
• SignType.neg_one_le 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : -1 ≤ a
• SignType.fin3Equiv 📋 Mathlib.Basic.Sign.Defs
  : SignType ≃* Fin 3
• SignType.neg_eq_self_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : -a = a ↔ a = 0
• SignType.self_eq_neg_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a = -a ↔ a = 0
• SignType.neg_le_neg_iff 📋 Mathlib.Basic.Sign.Defs
  {a b : SignType} : -a ≤ -b ↔ b ≤ a
• SignType.nonpos_iff_ne_one 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a ≤ 0 ↔ a ≠ 1
• SignType.one_le_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : 1 ≤ a ↔ a = 1
• SignType.neg_eq_zero_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : -a = 0 ↔ a = 0
• SignType.nonneg_iff_ne_neg_one 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : 0 ≤ a ↔ a ≠ -1
• SignType.not_one_lt 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : ¬1 < a
• SignType.sign 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] : α →o SignType
• SignType.coe_one 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] : ↑1 = 1
• SignType.coe_zero 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] : ↑0 = 0
• SignType.le_neg_one_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a ≤ -1 ↔ a = -1
• SignType.not_lt_neg_one 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : ¬a < -1
• SignType.neg_one_lt_one 📋 Mathlib.Basic.Sign.Defs
  : -1 < 1
• SignType.nonneg_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1
• SignType.coe_neg_one 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] : ↑(-1) = -1
• SignType.pos_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : 0 < a ↔ a = 1
• SignType.trichotomy 📋 Mathlib.Basic.Sign.Defs
  (a : SignType) : a = -1 ∨ a = 0 ∨ a = 1
• SignType.lt_one_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a < 1 ↔ a ≤ 0
• SignType.nonpos_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0
• SignType.neg_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : a < 0 ↔ a = -1
• SignType.neg_one_lt_iff 📋 Mathlib.Basic.Sign.Defs
  {a : SignType} : -1 < a ↔ 0 ≤ a
• SignType.neg_lt_neg_iff 📋 Mathlib.Basic.Sign.Defs
  {a b : SignType} : -a < -b ↔ b < a
• SignType.coe_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_2} [One α] [SubtractionMonoid α] (s : SignType) : ↑(-s) = -↑s
• sign_zero 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] : SignType.sign 0 = 0
• sign_pos 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : 0 < a) : SignType.sign a = 1
• sign_eq_one_iff 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = 1 ↔ 0 < a
• sign_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : a < 0) : SignType.sign a = -1
• sign_eq_neg_one_iff 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = -1 ↔ a < 0
• Int.sign_eq_sign 📋 Mathlib.Basic.Sign.Defs
  (n : ℤ) : n.sign = ↑(SignType.sign n)
• SignType.map_cast' 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [One α] [Neg α] {β : Type u_2} [One β] [Neg β] [Zero β] (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) : f ↑s = ↑s
• sign_one 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [DecidableLT α] [Nontrivial α] : SignType.sign 1 = 1
• sign_eq_zero_iff 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a = 0 ↔ a = 0
• sign_ne_zero 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a ≠ 0 ↔ a ≠ 0
• SignType.map_cast 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType) : f ↑s = ↑s
• sign_nonneg_iff 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : 0 ≤ SignType.sign a ↔ 0 ≤ a
• sign_nonpos_iff 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a ≤ 0 ↔ a ≤ 0
• sign_apply 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
• Left.sign_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddLeftStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a
• Right.sign_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddRightStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a
• StrictMono.sign_comp 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} {F : Type u_3} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono ⇑f) (a : α) : SignType.sign (f a) = SignType.sign a
• sign_eq_sign_or_eq_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [Zero α] [LinearOrder α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : SignType.sign a = SignType.sign b ∨ SignType.sign a = -SignType.sign b
• SignType.castHom 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] : SignType →*₀ α
• SignType.zpow_odd 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {z : ℤ} (hz : Odd z) : s ^ z = s
• SignType.pow_odd 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {n : ℕ} (hn : Odd n) : s ^ n = s
• signHom 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] : α →*₀ SignType
• SignType.range_eq 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} (f : SignType → α) : Set.range f = {f SignType.zero, f SignType.neg, f SignType.pos}
• SignType.zpow_even 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {z : ℤ} (hz : Even z) (hs : s ≠ 0) : s ^ z = 1
• SignType.pow_even 📋 Mathlib.Basic.Sign.Basic
  (s : SignType) {n : ℕ} (hn : Even n) (hs : s ≠ 0) : s ^ n = 1
• SignType.univ_eq 📋 Mathlib.Basic.Sign.Basic
  : Finset.univ = {0, -1, 1}
• SignType.intCast_cast 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [AddGroupWithOne α] (s : SignType) : ↑↑s = ↑s
• SignType.castHom_apply 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a✝ : SignType) : SignType.castHom a✝ = ↑a✝
• SignType.coe_mul 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a b : SignType) : ↑(a * b) = ↑a * ↑b
• SignType.coe_pow 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [MonoidWithZero α] [HasDistribNeg α] (a : SignType) (k : ℕ) : ↑(a ^ k) = ↑a ^ k
• exists_signed_sum 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [DecidableEq α] (s : Finset α) (f : α → ℤ) : ∃ β x sgn g, (∀ (b : β), g b ∈ s) ∧ Fintype.card β = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
• SignType.coe_zpow 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [GroupWithZero α] [HasDistribNeg α] (a : SignType) (k : ℤ) : ↑(a ^ k) = ↑a ^ k
• sign_intCast 📋 Mathlib.Basic.Sign.Basic
  {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] [DecidableLT α] (n : ℤ) : SignType.sign ↑n = SignType.sign n
• exists_signed_sum' 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ) (h : ∑ i ∈ s, (f i).natAbs ≤ n) : ∃ β x sgn g, (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then ↑(sgn i) else 0) = f a
• signHom_apply 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] : ⇑signHom = ⇑SignType.sign
• abs_mul_sign 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : |x| * ↑(SignType.sign x) = x
• self_mul_sign 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : x * ↑(SignType.sign x) = |x|
• sign_mul_abs 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : ↑(SignType.sign x) * |x| = x
• sign_mul_self 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : ↑(SignType.sign x) * x = |x|
• sign_pow 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) (n : ℕ) : SignType.sign (x ^ n) = SignType.sign x ^ n
• sign_sum 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {ι : Type u_1} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType) (h : ∀ i ∈ s, SignType.sign (f i) = t) : SignType.sign (∑ i ∈ s, f i) = t
• sign_mul 📋 Mathlib.Basic.Sign.Basic
  {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x y : α) : SignType.sign (x * y) = SignType.sign x * SignType.sign y
• EReal.coe_coe_sign 📋 Mathlib.Data.EReal.Inv
  (x : SignType) : ↑↑x = ↑x
• EReal.sign_top 📋 Mathlib.Data.EReal.Inv
  : SignType.sign ⊤ = 1
• EReal.sign_bot 📋 Mathlib.Data.EReal.Inv
  : SignType.sign ⊥ = -1
• EReal.abs_mul_sign 📋 Mathlib.Data.EReal.Inv
  (x : EReal) : ↑x.abs * ↑(SignType.sign x) = x
• EReal.sign_mul_abs 📋 Mathlib.Data.EReal.Inv
  (x : EReal) : ↑(SignType.sign x) * ↑x.abs = x
• EReal.sign_mul_inv_abs 📋 Mathlib.Data.EReal.Inv
  (a : EReal) : ↑(SignType.sign a) * (↑a.abs)⁻¹ = a⁻¹
• EReal.sign_mul_inv_abs' 📋 Mathlib.Data.EReal.Inv
  (a : EReal) : ↑(SignType.sign a) * ↑a.abs⁻¹ = a⁻¹
• EReal.sign_coe 📋 Mathlib.Data.EReal.Inv
  (x : ℝ) : SignType.sign ↑x = SignType.sign x
• EReal.sign_neg 📋 Mathlib.Data.EReal.Inv
  (x : EReal) : SignType.sign (-x) = -SignType.sign x
• EReal.sign_eq_and_abs_eq_iff_eq 📋 Mathlib.Data.EReal.Inv
  {x y : EReal} : x.abs = y.abs ∧ SignType.sign x = SignType.sign y ↔ x = y
• EReal.sign_mul 📋 Mathlib.Data.EReal.Inv
  (x y : EReal) : SignType.sign (x * y) = SignType.sign x * SignType.sign y
• EReal.le_iff_sign 📋 Mathlib.Data.EReal.Inv
  {x y : EReal} : x ≤ y ↔ SignType.sign x < SignType.sign y ∨ SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨ SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨ SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs
• instTopologicalSpaceSignType 📋 Mathlib.Topology.Instances.Sign
  : TopologicalSpace SignType
• instDiscreteTopologySignType 📋 Mathlib.Topology.Instances.Sign
  : DiscreteTopology SignType
• continuousAt_sign_of_neg 📋 Mathlib.Topology.Instances.Sign
  {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [OrderTopology α] {a : α} (h : a < 0) : ContinuousAt (⇑SignType.sign) a
• continuousAt_sign_of_pos 📋 Mathlib.Topology.Instances.Sign
  {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [OrderTopology α] {a : α} (h : 0 < a) : ContinuousAt (⇑SignType.sign) a
• continuousAt_sign_of_ne_zero 📋 Mathlib.Topology.Instances.Sign
  {α : Type u_1} [Zero α] [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : a ≠ 0) : ContinuousAt (⇑SignType.sign) a
• Real.Angle.sign 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : SignType
• Real.Angle.sign_coe_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : (↑Real.pi).sign = 0
• Real.Angle.sign_antiperiodic 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : Function.Antiperiodic Real.Angle.sign ↑Real.pi
• Real.Angle.coe_abs_toReal_of_sign_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} (h : 0 ≤ θ.sign) : ↑|θ.toReal| = θ
• Real.Angle.sign_pi_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (↑Real.pi - θ).sign = θ.sign
• Real.Angle.toReal_nonneg_iff_sign_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : 0 ≤ θ.toReal ↔ 0 ≤ θ.sign
• Real.Angle.sign_neg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (-θ).sign = -θ.sign
• Real.Angle.toReal_neg_iff_sign_neg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.toReal < 0 ↔ θ.sign = -1
• Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : θ.sign = ψ.sign) : θ = ψ ↔ |θ.toReal| = |ψ.toReal|
• Real.Angle.sign_sub_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ - ↑Real.pi).sign = -θ.sign
• Real.Angle.sign_zero 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : Real.Angle.sign 0 = 0
• Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} : θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|
• Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) : 0 ≤ (↑θ).sign
• Real.Angle.sign_add_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ + ↑Real.pi).sign = -θ.sign
• Real.Angle.sign_pi_add 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (↑Real.pi + θ).sign = -θ.sign
• Real.Angle.toReal_mem_Ioo_iff_sign_pos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.toReal ∈ Set.Ioo 0 Real.pi ↔ θ.sign = 1
• Real.Angle.neg_coe_abs_toReal_of_sign_nonpos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} (h : θ.sign ≤ 0) : -↑|θ.toReal| = θ
• Real.Angle.sign_coe_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : (↑(Real.pi / 2)).sign = 1
• Real.Angle.sign_eq_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.sign = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
• Real.Angle.sign_ne_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
• Real.Angle.sub_ne_pi_of_sign_eq_of_sign_ne_zero 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (a b : Real.Angle) (h_sign : a.sign = b.sign) (h_ne : b.sign ≠ 0) : a - b ≠ ↑Real.pi
• Real.Angle.continuousAt_sign 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} (h0 : θ ≠ 0) (hpi : θ ≠ ↑Real.pi) : ContinuousAt Real.Angle.sign θ
• Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) : (-↑θ).sign ≤ 0
• Real.Angle.sign_coe_neg_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : (↑(-Real.pi / 2)).sign = -1
• Real.Angle.sign_toReal 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} (h : θ ≠ ↑Real.pi) : SignType.sign θ.toReal = θ.sign
• Real.Angle.toReal_add_of_sign_eq_neg_sign 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (hψ : θ ≠ ↑Real.pi ∨ ψ ≠ ↑Real.pi) (hs : θ.sign = -ψ.sign) : (θ + ψ).toReal = θ.toReal + ψ.toReal
• Real.Angle.toReal_add_of_sign_pos_sign_neg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (hθ : θ.sign = 1) (hψ : ψ.sign = -1) : (θ + ψ).toReal = θ.toReal + ψ.toReal
• ContinuousOn.angle_sign_comp 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {α : Type u_1} [TopologicalSpace α] {f : α → Real.Angle} {s : Set α} (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) : ContinuousOn (Real.Angle.sign ∘ f) s
• Real.Angle.two_zsmul_eq_iff_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {a b : Real.Angle} (ha : a.sign ≠ 0) (h : a.sign = b.sign) : 2 • a = 2 • b ↔ a = b
• Real.Angle.sign_two_zsmul_eq_sign_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : (2 • θ).sign = θ.sign ↔ θ = ↑Real.pi ∨ |θ.toReal| < Real.pi / 2
• Real.Angle.toReal_add_eq_toReal_add_toReal 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (hθ : θ ≠ ↑Real.pi) (hψ : ψ ≠ ↑Real.pi) (hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign) : (θ + ψ).toReal = θ.toReal + ψ.toReal
• Real.Angle.sign_two_nsmul_eq_sign_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : (2 • θ).sign = θ.sign ↔ θ = ↑Real.pi ∨ |θ.toReal| < Real.pi / 2
• Real.Angle.sign_eq_of_continuousOn 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {α : Type u_1} [TopologicalSpace α] {f : α → Real.Angle} {s : Set α} {x y : α} (hc : IsConnected s) (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) (hx : x ∈ s) (hy : y ∈ s) : (f y).sign = (f x).sign
• Real.Angle.eq_add_pi_of_two_zsmul_eq_of_sign_eq_neg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (a b : Real.Angle) (h : 2 • a = 2 • b) (h_sign : a.sign = -b.sign) (h_ne : b.sign ≠ 0) : a = b + ↑Real.pi
• Real.Angle.sign_two_zsmul_eq_neg_sign_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ Real.pi / 2 < |θ.toReal|
• Real.Angle.sign_two_nsmul_eq_neg_sign_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ Real.pi / 2 < |θ.toReal|
• Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_zsmul_add_eq_zero_of_sign_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • (θ + ψ) = 0) (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) : |θ.toReal| + |ψ.toReal| = Real.pi
• Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • (θ + ψ) = 0) (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) : |θ.toReal| + |ψ.toReal| = Real.pi
• Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (hs : θ.sign = ψ.sign) (hsa : θ.sign ≠ (θ + ψ).sign) : |(θ + ψ).toReal| = 2 * Real.pi - (|θ.toReal| + |ψ.toReal|)
• sign_eq_of_affineCombination_mem_affineSpan_single_lineMap 📋 Mathlib.LinearAlgebra.AffineSpace.Independent
  {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) {i₁ i₂ i₃ : ι} (h₁ : i₁ ∈ s) (h₂ : i₂ ∈ s) (h₃ : i₃ ∈ s) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {c : k} (hc0 : 0 < c) (hc1 : c < 1) (hs : (Finset.affineCombination k s p) w ∈ line[k, p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c]) : SignType.sign (w i₂) = SignType.sign (w i₃)
• sign_eq_of_affineCombination_mem_affineSpan_pair 📋 Mathlib.LinearAlgebra.AffineSpace.Independent
  {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (hs : (Finset.affineCombination k s p) w ∈ line[k, (Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂]) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0) (hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)) : SignType.sign (w i) = SignType.sign (w j)
• Polynomial.signVariations_eraseLead 📋 Mathlib.Algebra.Polynomial.RuleOfSigns
  {R : Type u_1} [Semiring R] [LinearOrder R] (P : Polynomial R) (h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff) : P.eraseLead.signVariations = P.signVariations
• Polynomial.signVariations_eq_eraseLead_add_ite 📋 Mathlib.Algebra.Polynomial.RuleOfSigns
  {R : Type u_1} [Semiring R] [LinearOrder R] {P : Polynomial R} (h : P ≠ 0) : P.signVariations = P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
• NormedSpace.normalize_smul 📋 Mathlib.Analysis.Normed.Module.Normalize
  {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (r : ℝ) (x : V) : NormedSpace.normalize (r • x) = ↑(SignType.sign r) • NormedSpace.normalize x
• deriv_abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  (x : ℝ) : deriv (fun x => |x|) x = ↑(SignType.sign x)
• hasDerivAt_abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun x => |x|) (↑(SignType.sign x)) x
• hasStrictDerivAt_abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  {x : ℝ} (hx : x ≠ 0) : HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x
• hasDerivWithinAt_abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  (s : Set ℝ) {x : ℝ} (hx : x ≠ 0) : HasDerivWithinAt (fun x => |x|) (↑(SignType.sign x)) s x
• HasFDerivAt.abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} (hf : HasFDerivAt f f' x) (h₀ : f x ≠ 0) : HasFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x
• HasStrictFDerivAt.abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} (hf : HasStrictFDerivAt f f' x) (h₀ : f x ≠ 0) : HasStrictFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x
• HasFDerivWithinAt.abs 📋 Mathlib.Analysis.Calculus.Deriv.Abs
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E} {x : E} (hf : HasFDerivWithinAt f f' s x) (h₀ : f x ≠ 0) : HasFDerivWithinAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') s x
• eventually_nhdsWithin_sign_eq_of_deriv_neg 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv f x₀ < 0) (hx : f x₀ = 0) : ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x₀ - x)
• eventually_nhdsWithin_sign_eq_of_deriv_pos 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv f x₀ > 0) (hx : f x₀ = 0) : ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x - x₀)
• isLocalMax_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀) (hf : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : IsLocalMax f x₀
• isLocalMin_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀) (hf : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : IsLocalMin f x₀
• deriv_neg_left_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b < 0
• deriv_neg_right_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b < 0
• deriv_pos_left_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b > 0
• deriv_pos_right_of_sign_deriv 📋 Mathlib.Analysis.Calculus.DerivativeTest
  {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b > 0
• HasFDerivAt.hasFDerivAt_norm_smul 📋 Mathlib.Analysis.Calculus.FDeriv.Norm
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ} (ht : t ≠ 0) (h : HasFDerivAt (fun x => ‖x‖) f x) : HasFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)
• HasStrictFDerivAt.hasStrictFDerivAt_norm_smul 📋 Mathlib.Analysis.Calculus.FDeriv.Norm
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ} (ht : t ≠ 0) (h : HasStrictFDerivAt (fun x => ‖x‖) f x) : HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)
• fderiv_norm_smul 📋 Mathlib.Analysis.Calculus.FDeriv.Norm
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (t : ℝ) : fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x
• Matrix.ProjGenLinGroup.signDet 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
  {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] : Matrix.ProjGenLinGroup n R →* SignTypeˣ
• Matrix.ProjGenLinGroup.val_signDet_mk 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
  {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) : ↑(Matrix.ProjGenLinGroup.signDet (Matrix.ProjGenLinGroup.mk g)) = SignType.sign ↑(Matrix.GeneralLinearGroup.det g)
• Matrix.ProjGenLinGroup.signDet_mk 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
  {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) : Matrix.ProjGenLinGroup.signDet (Matrix.ProjGenLinGroup.mk g) = (Units.map ↑signHom) (Matrix.GeneralLinearGroup.det g)
• UpperHalfPlane.det_smulFDeriv 📋 Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
  (g : GL (Fin 2) ℝ) (z : ℂ) : (UpperHalfPlane.smulFDeriv g z).det = ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖UpperHalfPlane.denom g z‖ ^ 4
• Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq 📋 Mathlib.Analysis.Convex.Side
  {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j, w₁ j = 1) (hw₂ : ∑ j, w₂ j = 1) {i : Fin (n + 1)} (hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)) (h0 : w₁ i ≠ 0) : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂)
• Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff 📋 Mathlib.Analysis.Convex.Side
  {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j, w₁ j = 1) (hw₂ : ∑ j, w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∧ w₁ i ≠ 0
• Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff 📋 Mathlib.Analysis.Convex.Side
  {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j, w₁ j = 1) (hw₂ : ∑ j, w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
• Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff 📋 Mathlib.Analysis.Convex.Side
  {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j, w₁ j = 1) (hw₂ : ∑ j, w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0
• Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff 📋 Mathlib.Analysis.Convex.Side
  {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j, w₁ j = 1) (hw₂ : ∑ j, w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0
• Orientation.ne_of_oangle_sign_eq_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ y
• Orientation.ne_of_oangle_sign_ne_zero 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ y
• Orientation.ne_of_oangle_sign_eq_neg_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ y
• Orientation.oangle_eq_angle_of_sign_eq_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign = 1) : o.oangle x y = ↑(InnerProductGeometry.angle x y)
• Orientation.oangle_sign_sub_left 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle (x - y) y).sign = (o.oangle x y).sign
• Orientation.oangle_sign_sub_left_swap 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle (x - y) x).sign = (o.oangle x y).sign
• Orientation.oangle_sign_sub_right 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle x (y - x)).sign = (o.oangle x y).sign
• Orientation.oangle_sign_sub_right_swap 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle y (y - x)).sign = (o.oangle x y).sign
• Orientation.left_ne_zero_of_oangle_sign_eq_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ 0
• Orientation.left_ne_zero_of_oangle_sign_ne_zero 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ 0
• Orientation.oangle_sign_add_left 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle (x + y) y).sign = (o.oangle x y).sign
• Orientation.oangle_sign_add_right 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle x (x + y)).sign = (o.oangle x y).sign
• Orientation.oangle_sign_neg_left 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign
• Orientation.oangle_sign_neg_right 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign
• Orientation.right_ne_zero_of_oangle_sign_eq_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign = 1) : y ≠ 0
• Orientation.right_ne_zero_of_oangle_sign_ne_zero 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : (o.oangle x y).sign ≠ 0) : y ≠ 0
• Orientation.oangle_sign_sub_left_eq_neg 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle (y - x) y).sign = -(o.oangle x y).sign
• Orientation.oangle_sign_sub_right_eq_neg 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) : (o.oangle x (x - y)).sign = -(o.oangle x y).sign

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c