Loogle!

Result

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

• Int.negInduction 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} (nat : (n : ℕ) → motive ↑n) (neg : ((n : ℕ) → motive ↑n) → (n : ℕ) → motive (-↑n)) (n : ℤ) : motive n
• Int.inductionOn'.neg 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)) (n : ℕ) : motive (b + Int.negSucc n)
• Int.inductionOn'.pos 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (n : ℕ) : motive (b + ↑n)
• Int.le_induction 📋 Mathlib.Data.Int.Init
  {m : ℤ} {motive : (n : ℤ) → m ≤ n → Prop} (base : motive m ⋯) (succ : ∀ (n : ℤ) (hmn : m ≤ n), motive n hmn → motive (n + 1) ⋯) (n : ℤ) (hmn : m ≤ n) : motive n hmn
• Int.inductionOn' 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} (z b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)) : motive z
• Int.inductionOn'_self 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} {b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)} {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} : Int.inductionOn' b b zero succ pred = zero
• Int.induction_on 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Prop} (i : ℤ) (zero : motive 0) (succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)) (pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)) : motive i
• Int.le_induction_down 📋 Mathlib.Data.Int.Init
  {m : ℤ} {motive : (n : ℤ) → n ≤ m → Prop} (base : motive m ⋯) (pred : ∀ (n : ℤ) (hmn : n ≤ m), motive n hmn → motive (n - 1) ⋯) (n : ℤ) (hmn : n ≤ m) : motive n hmn
• Int.inductionOn'_sub_one 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} {z b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)} {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} (hz : z ≤ b) : Int.inductionOn' (z - 1) b zero succ pred = pred z hz (Int.inductionOn' z b zero succ pred)
• Int.inductionOn'.eq_1 📋 Mathlib.Data.Int.Init
  {motive : ℤ → Sort u_1} (z b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)) : Int.inductionOn' z b zero succ pred = cast ⋯ (match z - b with | Int.ofNat n => Int.inductionOn'.pos b zero succ n | Int.negSucc n => Int.inductionOn'.neg b zero pred 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) : Int.inductionOn' (z + 1) b H0 Hs Hp = Hs z hz (Int.inductionOn' z 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 66afee5 serving mathlib revision f3731ea