Loogle!

Result

Found 290 declarations whose name contains "sub_eq". Of these, 62 have a name containing "sub_eq" and "iff".

• Nat.sub_eq_iff_eq_add 📋 Init.Data.Nat.Basic
  {b a c : ℕ} (h : b ≤ a) : a - b = c ↔ a = c + b
• Nat.sub_eq_iff_eq_add' 📋 Init.Data.Nat.Basic
  {b a c : ℕ} (h : b ≤ a) : a - b = c ↔ a = b + c
• Int.sub_eq_iff_eq_add 📋 Init.Data.Int.Lemmas
  {b a c : ℤ} : a - b = c ↔ a = c + b
• Int.sub_eq_iff_eq_add' 📋 Init.Data.Int.Lemmas
  {b a c : ℤ} : a - b = c ↔ a = b + c
• Nat.sub_eq_zero_iff_le 📋 Init.Data.Nat.Lemmas
  {n m : ℕ} : n - m = 0 ↔ n ≤ m
• Int.bmod_eq_bmod_iff_bmod_sub_eq_zero 📋 Init.Data.Int.DivMod.Lemmas
  {m : ℤ} {n : ℕ} {k : ℤ} : m.bmod n = k.bmod n ↔ (m - k).bmod n = 0
• Int.fmod_eq_fmod_iff_fmod_sub_eq_zero 📋 Init.Data.Int.DivMod.Lemmas
  {m n k : ℤ} : m.fmod n = k.fmod n ↔ (m - k).fmod n = 0
• Int.emod_eq_emod_iff_emod_sub_eq_zero 📋 Init.Data.Int.DivMod.Lemmas
  {m n k : ℤ} : m % n = k % n ↔ (m - k) % n = 0
• BitVec.sub_eq_iff_eq_add 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x y z : BitVec w} : x - y = z ↔ x = z + y
• UInt16.sub_eq_iff_eq_add 📋 Init.Data.UInt.Lemmas
  {a b c : UInt16} : a - b = c ↔ a = c + b
• UInt32.sub_eq_iff_eq_add 📋 Init.Data.UInt.Lemmas
  {a b c : UInt32} : a - b = c ↔ a = c + b
• UInt64.sub_eq_iff_eq_add 📋 Init.Data.UInt.Lemmas
  {a b c : UInt64} : a - b = c ↔ a = c + b
• UInt8.sub_eq_iff_eq_add 📋 Init.Data.UInt.Lemmas
  {a b c : UInt8} : a - b = c ↔ a = c + b
• USize.sub_eq_iff_eq_add 📋 Init.Data.UInt.Lemmas
  {a b c : USize} : a - b = c ↔ a = c + b
• Lean.Grind.AddCommGroup.sub_eq_zero_iff 📋 Init.Grind.Module.Basic
  {M : Type u} [Lean.Grind.AddCommGroup M] {a b : M} : a - b = 0 ↔ a = b
• Lean.Grind.AddCommGroup.sub_eq_iff 📋 Init.Grind.Module.Basic
  {M : Type u} [Lean.Grind.AddCommGroup M] {a b c : M} : a - b = c ↔ a = c + b
• ISize.sub_eq_iff_eq_add 📋 Init.Data.SInt.Lemmas
  {a b c : ISize} : a - b = c ↔ a = c + b
• Int16.sub_eq_iff_eq_add 📋 Init.Data.SInt.Lemmas
  {a b c : Int16} : a - b = c ↔ a = c + b
• Int32.sub_eq_iff_eq_add 📋 Init.Data.SInt.Lemmas
  {a b c : Int32} : a - b = c ↔ a = c + b
• Int64.sub_eq_iff_eq_add 📋 Init.Data.SInt.Lemmas
  {a b c : Int64} : a - b = c ↔ a = c + b
• Int8.sub_eq_iff_eq_add 📋 Init.Data.SInt.Lemmas
  {a b c : Int8} : a - b = c ↔ a = c + b
• Std.Tactic.BVDecide.Frontend.Normalize.BitVec.sub_eq_iff_eq_add 📋 Std.Tactic.BVDecide.Normalize.Equal
  {w : ℕ} (a b c : BitVec w) : (a + (~~~b + 1#w) == c) = (a == c + b)
• eq_iff_eq_of_sub_eq_sub 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddGroup G] {a b c d : G} (H : a - b = c - d) : a = b ↔ c = d
• sub_eq_iff_eq_add 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddGroup G] {a b c : G} : a - b = c ↔ a = c + b
• sub_eq_iff_eq_add' 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddCommGroup G] {a b c : G} : a - b = c ↔ a = b + c
• sub_eq_sub_iff_comm 📋 Mathlib.Algebra.Group.Basic
  {α : Type u_1} [SubtractionMonoid α] (a b c : α) {d : α} : a - b = c - d ↔ b - a = d - c
• sub_eq_sub_iff_sub_eq_sub 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddCommGroup G] {a b c d : G} : a - b = c - d ↔ a - c = b - d
• sub_eq_sub_iff_add_eq_add 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddCommGroup G] {a b c d : G} : a - b = c - d ↔ a + d = c + b
• IsAddUnit.sub_eq_zero_iff_eq 📋 Mathlib.Algebra.Group.Units.Basic
  {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) : a - b = 0 ↔ a = b
• IsAddUnit.sub_eq_iff 📋 Mathlib.Algebra.Group.Units.Basic
  {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) : a - b = c ↔ a = c + b
• IsAddUnit.sub_eq_sub_iff 📋 Mathlib.Algebra.Group.Units.Basic
  {α : Type u} [SubtractionCommMonoid α] {a b c d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) : a - b = c - d ↔ a + d = c + b
• AddCommute.sub_eq_sub_iff_of_isAddUnit 📋 Mathlib.Algebra.Group.Commute.Units
  {M : Type u_1} [SubtractionMonoid M] {a b c d : M} (hbd : AddCommute b d) (hb : IsAddUnit b) (hd : IsAddUnit d) : a - b = c - d ↔ a + d = c + b
• WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {G : Type u_1} [AddCommGroup G] {x y : WithTop G} : x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤
• tsub_eq_iff_eq_add_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b = c ↔ a = c + b
• AddLECancellable.tsub_eq_iff_eq_add_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : b ≤ a) : a - b = c ↔ a = c + b
• tsub_eq_zero_iff_le 📋 Mathlib.Algebra.Order.Sub.Basic
  {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - b = 0 ↔ a ≤ b
• vsub_eq_zero_iff_eq 📋 Mathlib.Algebra.AddTorsor.Defs
  {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P} : p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂
• eq_vadd_iff_vsub_eq 📋 Mathlib.Algebra.AddTorsor.Defs
  {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ : P) (g : G) (p₂ : P) : p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g
• vadd_eq_vadd_iff_sub_eq_vsub 📋 Mathlib.Algebra.AddTorsor.Basic
  {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] {v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
• AddOreLocalization.oreSub_eq_iff 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ r₂ : X} {s₁ s₂ : ↥S} : r₁ -ₒ s₁ = r₂ -ₒ s₂ ↔ ∃ u v, u +ᵥ r₂ = v +ᵥ r₁ ∧ ↑u + ↑s₂ = v + ↑s₁
• WithTop.sub_eq_top_iff 📋 Mathlib.Algebra.Order.Sub.WithTop
  {α : Type u_1} [Sub α] [Bot α] {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
• ENat.sub_eq_top_iff 📋 Mathlib.Data.ENat.Basic
  {a b : ℕ∞} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
• Ordinal.sub_eq_zero_iff_le 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} : a - b = 0 ↔ a ≤ b
• Ordinal.lsub_eq_zero_iff 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max v u_4}) : Ordinal.lsub f = 0 ↔ IsEmpty ι
• Ordinal.blsub_eq_zero_iff 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}} : o.blsub f = 0 ↔ o = 0
• Ordinal.isNormal_iff_lt_succ_and_blsub_eq 📋 Mathlib.SetTheory.Ordinal.Family
  {f : Ordinal.{u} → Ordinal.{max u v}} : Order.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.blsub fun x x_1 => f x) = f o
• AbsoluteValue.map_sub_eq_zero_iff 📋 Mathlib.Algebra.Order.AbsoluteValue.Basic
  {R : Type u_5} {S : Type u_6} [Ring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (a b : R) : abv (a - b) = 0 ↔ a = b
• ENNReal.sub_eq_top_iff 📋 Mathlib.Data.ENNReal.Operations
  {a b : ENNReal} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
• Filter.vsub_eq_bot_iff 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
• Filter.sub_eq_bot_iff 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Sub α] {f g : Filter α} : f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥
• norm_sub_eq_zero_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_5} [NormedAddGroup E] {a b : E} : ‖a - b‖ = 0 ↔ a = b
• Complex.exp_eq_exp_iff_exp_sub_eq_one 📋 Mathlib.Analysis.SpecialFunctions.Complex.Log
  {x y : ℂ} : Complex.exp x = Complex.exp y ↔ Complex.exp (x - y) = 1
• midpoint_eq_midpoint_iff_vsub_eq_vsub 📋 Mathlib.LinearAlgebra.AffineSpace.Midpoint
  (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x x' y y' : P} : midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
• real_inner_add_sub_eq_zero_iff 📋 Mathlib.Analysis.InnerProductSpace.Basic
  {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : inner ℝ (x + y) (x - y) = 0 ↔ ‖x‖ = ‖y‖
• norm_sub_eq_sqrt_iff_real_inner_eq_zero 📋 Mathlib.Analysis.InnerProductSpace.Basic
  {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} : ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ inner ℝ x y = 0
• eventuallyConst_iff_analyticOrderAt_sub_eq_top 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} : Filter.EventuallyConst f (nhds z₀) ↔ analyticOrderAt (fun x => f x - f z₀) z₀ = ⊤
• Affine.Simplex.eq_centroid_iff_sum_vsub_eq_zero 📋 Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
  {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] {s : Affine.Simplex k P n} {p : P} : p = s.centroid ↔ ∑ i, (s.points i -ᵥ p) = 0
• InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ‖x - y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi
• InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ‖x - y‖ = |‖x‖ - ‖y‖| ↔ InnerProductGeometry.angle x y = 0
• Complex.norm_sub_eq_iff 📋 Mathlib.Analysis.Complex.Arg
  {x y : ℂ} : ‖x - y‖ = |‖x‖ - ‖y‖| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
• eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top 📋 Mathlib.Analysis.Meromorphic.Order
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} : Filter.EventuallyConst f (nhdsWithin x {x}ᶜ) ↔ ∃ c, meromorphicOrderAt (fun x => f x - c) x = ⊤
• AffineSubspace.mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero 📋 Mathlib.Geometry.Euclidean.PerpBisector
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c p₁ p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ ((Equiv.pointReflection c) p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = 0

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 6ff4759 serving mathlib revision 76f94b4