Loogle!

Result

Found 12164 declarations mentioning Int. Of these, 20 have a name containing "induction".

• Int.negInduction 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} (nat : (n : ℕ) → C ↑n) (neg : ((n : ℕ) → C ↑n) → (n : ℕ) → C (-↑n)) (n : ℤ) : C n
• Int.le_induction 📋 Mathlib.Data.Int.Init
  {P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n
• Int.le_induction_down 📋 Mathlib.Data.Int.Init
  {P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ n ≤ m, P n → P (n - 1)) (n : ℤ) : n ≤ m → P n
• Int.inductionOn'.neg 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) (n : ℕ) : C (b + Int.negSucc n)
• Int.inductionOn'.pos 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (n : ℕ) : C (b + ↑n)
• Int.inductionOn' 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} (z b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) : C z
• Int.inductionOn'_self 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} {b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} : b.inductionOn' b H0 Hs Hp = H0
• Int.induction_on 📋 Mathlib.Data.Int.Init
  {p : ℤ → Prop} (i : ℤ) (hz : p 0) (hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)) (hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)) : p i
• Int.inductionOn'_sub_one 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} {z b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} (hz : z ≤ b) : (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)
• Int.inductionOn'.eq_1 📋 Mathlib.Data.Int.Init
  {C : ℤ → Sort u_1} (z b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) : z.inductionOn' b H0 Hs Hp = cast ⋯ (match z - b with | Int.ofNat n => Int.inductionOn'.pos b H0 Hs n | Int.negSucc n => Int.inductionOn'.neg b H0 Hp n)
• zpow_induction_left 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (g * a)) (h_inv : ∀ (a : G), P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n)
• zpow_induction_right 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (a * g)) (h_inv : ∀ (a : G), P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n)
• zsmul_induction_left 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddGroup G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (g + a)) (h_inv : ∀ (a : G), P a → P (-g + a)) (n : ℤ) : P (n • g)
• zsmul_induction_right 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddGroup G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (a + g)) (h_inv : ∀ (a : G), P a → P (a + -g)) (n : ℤ) : P (n • g)
• Int.inductionOn'_add_one 📋 Mathlib.Data.Int.Basic
  {C : ℤ → Sort u_1} {z b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} (hz : b ≤ z) : (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)
• LaurentPolynomial.induction_on_mul_T 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] {Q : LaurentPolynomial R → Prop} (f : LaurentPolynomial R) (Qf : ∀ {f : Polynomial R} {n : ℕ}, Q (Polynomial.toLaurent f * LaurentPolynomial.T (-↑n))) : Q f
• LaurentPolynomial.induction_on' 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] {motive : LaurentPolynomial R → Prop} (p : LaurentPolynomial R) (add : ∀ (p q : LaurentPolynomial R), motive p → motive q → motive (p + q)) (C_mul_T : ∀ (n : ℤ) (a : R), motive (LaurentPolynomial.C a * LaurentPolynomial.T n)) : motive p
• LaurentPolynomial.induction_on 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] {M : LaurentPolynomial R → Prop} (p : LaurentPolynomial R) (h_C : ∀ (a : R), M (LaurentPolynomial.C a)) (h_add : ∀ {p q : LaurentPolynomial R}, M p → M q → M (p + q)) (h_C_mul_T : ∀ (n : ℕ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T ↑n) → M (LaurentPolynomial.C a * LaurentPolynomial.T (↑n + 1))) (h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n)) → M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n - 1))) : M p
• FixedDetMatrices.induction_on 📋 Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
  {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop} {A : FixedDetMatrix (Fin 2) ℤ m} (hm : m ≠ 0) (h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A) (hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) (hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.T • B)) : C A
• Poly.induction 📋 Mathlib.NumberTheory.Dioph
  {α : Type u_1} {C : Poly α → Prop} (H1 : ∀ (i : α), C (Poly.proj i)) (H2 : ∀ (n : ℤ), C (Poly.const n)) (H3 : ∀ (f g : Poly α), C f → C g → C (f - g)) (H4 : ∀ (f g : Poly α), C f → C g → C (f * g)) (f : Poly α) : C f

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 19971e9 serving mathlib revision e0654b0