Loogle!

Result

Found 168 declarations mentioning Int.negSucc.

• Int.negSucc 📋 Init.Data.Int.Basic
  : ℕ → ℤ
• Int.negSucc.injEq 📋 Init.Data.Int.Basic
  (a✝ a✝¹ : ℕ) : (Int.negSucc a✝ = Int.negSucc a✝¹) = (a✝ = a✝¹)
• Int.negSucc.sizeOf_spec 📋 Init.Data.Int.Basic
  (a✝ : ℕ) : sizeOf (Int.negSucc a✝) = 1 + sizeOf a✝
• Int.fdiv.eq_4 📋 Init.Data.Int.DivMod.Basic
  (a : ℕ) : (Int.negSucc a).fdiv 0 = 0
• Int.fdiv.eq_3 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.ofNat m.succ).fdiv (Int.negSucc n) = Int.negSucc (m / n.succ)
• Int.fdiv.eq_5 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.negSucc m).fdiv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
• Int.fdiv.eq_6 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.negSucc m).fdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
• Int.negSucc_emod_ofNat 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a % ↑b = Int.subNatNat b (a % b).succ
• Int.negSucc_ediv_ofNat_succ 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a / ↑(b + 1) = Int.negSucc (a / b.succ)
• Int.ofNat_ediv_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.ofNat a / Int.negSucc b = -↑(a / (b + 1))
• Int.negSucc_ediv_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a / Int.negSucc b = ↑(a / (b + 1) + 1)
• Int.negSucc_emod_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a % Int.negSucc b = Int.subNatNat (b + 1) (a % (b + 1)).succ
• Int.negSucc_ne_zero 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n ≠ 0
• Int.zero_ne_negSucc 📋 Init.Data.Int.Lemmas
  (n : ℕ) : 0 ≠ Int.negSucc n
• Int.negSucc_inj 📋 Init.Data.Int.Lemmas
  {m n : ℕ} : Int.negSucc m = Int.negSucc n ↔ m = n
• Int.neg_ofNat_succ 📋 Init.Data.Int.Lemmas
  (n : ℕ) : -↑n.succ = Int.negSucc n
• Int.negSucc_add_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m + ↑n = Int.subNatNat n m.succ
• Int.ofNat_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m + Int.negSucc n = Int.subNatNat m n.succ
• Int.subNatNat_of_lt 📋 Init.Data.Int.Lemmas
  {m n : ℕ} (h : m < n) : Int.subNatNat m n = Int.negSucc (n - m).pred
• Int.subNatNat_of_sub_eq_succ 📋 Init.Data.Int.Lemmas
  {m n k : ℕ} (h : n - m = k.succ) : Int.subNatNat m n = Int.negSucc k
• Int.negSucc_eq 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n = -(↑n + 1)
• Int.neg_negSucc 📋 Init.Data.Int.Lemmas
  (n : ℕ) : -Int.negSucc n = ↑(n + 1)
• Int.negOfNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)
• Int.negSucc_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m + Int.negSucc n = Int.negSucc (m + n).succ
• Int.negSucc_mul_negOfNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)
• Int.subNatNat_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + k.succ)
• Int.subNatNat_add_right 📋 Init.Data.Int.Lemmas
  {m n : ℕ} : Int.subNatNat m (m + n + 1) = Int.negSucc n
• Int.negSucc_add_one_eq_neg_ofNat_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : Int.negSucc a + 1 = -↑b ↔ a = b
• Int.negSucc_eq_neg_ofNat_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : Int.negSucc a = -↑b ↔ a + 1 = b
• Int.neg_ofNat_eq_negSucc_add_one_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : -↑a = Int.negSucc b + 1 ↔ a = b
• Int.neg_ofNat_eq_negSucc_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : -↑a = Int.negSucc b ↔ a = b + 1
• Int.negSucc_sub_one 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n - 1 = Int.negSucc (n + 1)
• Int.ofNat_add_negSucc_of_lt 📋 Init.Data.Int.Lemmas
  {m n : ℕ} (h : m < n.succ) : Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)
• Int.negSucc_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
• Int.negSucc_mul_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * ↑n = -↑(m.succ * n)
• Int.ofNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m * Int.negSucc n = -↑(m * n.succ)
• Int.subNatNat.eq_1 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.subNatNat m n = match n - m with | 0 => Int.ofNat (m - n) | k.succ => Int.negSucc k
• Int.negSucc_mul_subNatNat 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
• Int.subNatNat_elim 📋 Init.Data.Int.Lemmas
  (m n : ℕ) (motive : ℕ → ℕ → ℤ → Prop) (hp : ∀ (i n : ℕ), motive (n + i) n ↑i) (hn : ∀ (i m : ℕ), motive m (m + i + 1) (Int.negSucc i)) : motive m n (Int.subNatNat m n)
• Int.natAbs_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : (Int.negSucc n).natAbs = n.succ
• Int.natAbs.eq_2 📋 Init.Data.Int.Order
  (n_1 : ℕ) : (Int.negSucc n_1).natAbs = n_1.succ
• Int.toNat?.eq_2 📋 Init.Data.Int.Order
  (a : ℕ) : (Int.negSucc a).toNat? = none
• Int.negSucc_le_zero 📋 Init.Data.Int.Order
  (n : ℕ) : Int.negSucc n ≤ 0
• Int.negSucc_lt_zero 📋 Init.Data.Int.Order
  (n : ℕ) : Int.negSucc n < 0
• Int.toNat_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : (Int.negSucc n).toNat = 0
• Int.toNat.eq_2 📋 Init.Data.Int.Order
  (a : ℕ) : (Int.negSucc a).toNat = 0
• Int.negSucc_not_nonneg 📋 Init.Data.Int.Order
  (n : ℕ) : 0 ≤ Int.negSucc n ↔ False
• Int.negSucc_not_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < Int.negSucc n ↔ False
• Int.sign_negSucc 📋 Init.Data.Int.Order
  (x : ℕ) : (Int.negSucc x).sign = -1
• Int.sign.eq_3 📋 Init.Data.Int.Order
  (a : ℕ) : (Int.negSucc a).sign = -1
• Int.eq_negSucc_of_lt_zero 📋 Init.Data.Int.Order
  {a : ℤ} : a < 0 → ∃ n, a = Int.negSucc n
• Int.negSucc_max_zero 📋 Init.Data.Int.Order
  (n : ℕ) : max (Int.negSucc n) 0 = 0
• Int.zero_max_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : max 0 (Int.negSucc n) = 0
• Int.mul.eq_2 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.ofNat m_2).mul (Int.negSucc n_2) = Int.negOfNat (m_2 * n_2.succ)
• Int.mul.eq_3 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.negSucc m_2).mul (Int.ofNat n_2) = Int.negOfNat (m_2.succ * n_2)
• Int.mul.eq_4 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.negSucc m_2).mul (Int.negSucc n_2) = Int.ofNat (m_2.succ * n_2.succ)
• Int.ediv.eq_3 📋 Init.Data.Int.DivMod.Bootstrap
  (a : ℕ) : (Int.negSucc a).ediv 0 = 0
• Int.ediv.eq_4 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.negSucc m).ediv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
• Int.ediv.eq_5 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.negSucc m).ediv (Int.negSucc n) = Int.ofNat (m / n.succ).succ
• Int.ediv.eq_2 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.ofNat m).ediv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• Int.negSucc_pow 📋 Init.Data.Int.Pow
  (m n : ℕ) : Int.negSucc m ^ n = if n % 2 = 0 then Int.ofNat (m.succ ^ n) else Int.negOfNat (m.succ ^ n)
• Int.tmod.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m).tmod (Int.negSucc n) = Int.ofNat (m % n.succ)
• Int.fmod.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).fmod (Int.ofNat n) = Int.subNatNat n (m % n).succ
• Int.tdiv.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
• Int.emod.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (x✝ : ℤ) (m : ℕ) : (Int.negSucc m).emod x✝ = Int.subNatNat x✝.natAbs (m % x✝.natAbs).succ
• Int.fmod.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m.succ).fmod (Int.negSucc n) = Int.subNatNat (m % n.succ) n
• Int.tdiv.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m).tdiv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• Int.tdiv.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tdiv (Int.ofNat n) = -Int.ofNat (m.succ / n)
• Int.tmod.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tmod (Int.ofNat n) = -Int.ofNat (m.succ % n)
• Int.fmod.eq_5 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).fmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
• Int.tmod.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
• Int.emod_negSucc 📋 Init.Data.Int.DivMod.Lemmas
  (m : ℕ) (n : ℤ) : Int.negSucc m % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
• Int.dvd_negSucc 📋 Init.Data.Int.DivMod.Lemmas
  {a : ℤ} {b : ℕ} : a ∣ Int.negSucc b ↔ a ∣ ↑(b + 1)
• Int.negSucc_dvd 📋 Init.Data.Int.DivMod.Lemmas
  {a : ℕ} {b : ℤ} : Int.negSucc a ∣ b ↔ ↑(a + 1) ∣ b
• Int.negSucc_ediv 📋 Init.Data.Int.DivMod.Lemmas
  (m : ℕ) {b : ℤ} (H : 0 < b) : Int.negSucc m / b = -((↑m).ediv b + 1)
• Int.negSucc_emod 📋 Init.Data.Int.DivMod.Lemmas
  (m : ℕ) {b : ℤ} (bpos : 0 < b) : Int.negSucc m % b = b - 1 - ↑m % b
• Int.negSucc_emod_negSucc_eq_zero_iff 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℕ} : Int.negSucc a % Int.negSucc b = 0 ↔ (a + 1) % (b + 1) = 0
• Int.negSucc_emod_ofNat_succ_eq_zero_iff 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℕ} : Int.negSucc a % (↑b + 1) = 0 ↔ (a + 1) % (b + 1) = 0
• Int.shiftRight.eq_2 📋 Init.Data.Int.Bitwise.Lemmas
  (x✝ n : ℕ) : (Int.negSucc n).shiftRight x✝ = Int.negSucc (n >>> x✝)
• Int.negSucc_shiftRight 📋 Init.Data.Int.Bitwise.Lemmas
  (m n : ℕ) : Int.negSucc m >>> n = Int.negSucc (m >>> n)
• Int.shiftLeft.eq_2 📋 Init.Data.Int.Bitwise.Lemmas
  (x✝ n : ℕ) : (Int.negSucc n).shiftLeft x✝ = Int.negSucc ((n + 1) <<< x✝ - 1)
• BitVec.ofInt_negSucc_eq_not_ofNat 📋 Init.Data.BitVec.Lemmas
  {w n : ℕ} : BitVec.ofInt w (Int.negSucc n) = ~~~BitVec.ofNat w n
• Rat.divInt.eq_2 📋 Init.Data.Rat.Lemmas
  (x✝ : ℤ) (d : ℕ) : Rat.divInt x✝ (Int.negSucc d) = Rat.normalize (-x✝) d.succ ⋯
• Rat.toDyadic.eq_2 📋 Init.Data.Dyadic.Basic
  (x : ℚ) (n : ℕ) : x.toDyadic (Int.negSucc n) = Dyadic.ofIntWithPrec (x.num / ↑(x.den <<< (n + 1))) (Int.negSucc n)
• Dyadic.toRat.eq_3 📋 Init.Data.Dyadic.Basic
  (n : ℤ) (k : ℕ) (hn : n % 2 = 1) : (Dyadic.ofOdd n (Int.negSucc k) hn).toRat = ↑(n * ↑(2 ^ (k + 1)))
• Int.testBit.eq_2 📋 Batteries.Data.Int
  (x✝ m : ℕ) : (Int.negSucc m).testBit x✝ = !m.testBit x✝
• DivInvMonoid.zpow_neg' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• SubNegMonoid.zsmul_neg' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : SubNegMonoid G] (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• negSucc_zsmul 📋 Mathlib.Algebra.Group.Defs
  {G : Type u_2} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a)
• zpow_negSucc 📋 Mathlib.Algebra.Group.Defs
  {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
• DivInvMonoid.mk 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [toMonoid : Monoid G] [toInv : Inv G] [toDiv : Div G] (div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G → G) (zpow_zero' : ∀ (a : G), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) : DivInvMonoid G
• SubNegMonoid.mk 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [toAddMonoid : AddMonoid G] [toNeg : Neg G] [toSub : Sub G] (sub_eq_add_neg : ∀ (a b : G), a - b = a + -b := by intros; rfl) (zsmul : ℤ → G → G) (zsmul_zero' : ∀ (a : G), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : G), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : G), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) : SubNegMonoid G
• Int.gcd_negSucc_ofNat 📋 Mathlib.Data.Int.Init
  (m n : ℕ) : (Int.negSucc m).gcd ↑n = (m + 1).gcd n
• Int.gcd_ofNat_negSucc 📋 Mathlib.Data.Int.Init
  (m n : ℕ) : (↑m).gcd (Int.negSucc n) = m.gcd (n + 1)
• Int.ofNat_add_negSucc_of_ge 📋 Mathlib.Data.Int.Init
  {m n : ℕ} (h : n.succ ≤ m) : Int.ofNat m + Int.negSucc n = Int.ofNat (m - n.succ)
• Int.gcd_negSucc_negSucc 📋 Mathlib.Data.Int.Init
  (m n : ℕ) : (Int.negSucc m).gcd (Int.negSucc n) = (m + 1).gcd (n + 1)
• 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)
• CommGroupWithZero.zpow_neg' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u_2} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (Int.negSucc n) a = (CommGroupWithZero.zpow (↑n.succ) a)⁻¹
• GroupWithZero.zpow_neg' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀) : GroupWithZero.zpow (Int.negSucc n) a = (GroupWithZero.zpow (↑n.succ) a)⁻¹
• GroupWithZero.mk 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u} [toMonoidWithZero : MonoidWithZero G₀] [toInv : Inv G₀] [toDiv : Div G₀] (div_eq_mul_inv : ∀ (a b : G₀), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G₀ → G₀) (zpow_zero' : ∀ (a : G₀), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G₀), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial G₀] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) : GroupWithZero G₀
• CommGroupWithZero.mk 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u_2} [toCommMonoidWithZero : CommMonoidWithZero G₀] [toInv : Inv G₀] [toDiv : Div G₀] (div_eq_mul_inv : ∀ (a b : G₀), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G₀ → G₀) (zpow_zero' : ∀ (a : G₀), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G₀), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial G₀] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) : CommGroupWithZero G₀
• AddGroupWithOne.zsmul_neg' 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [self : AddGroupWithOne R] (n : ℕ) (a : R) : AddGroupWithOne.zsmul (Int.negSucc n) a = -AddGroupWithOne.zsmul (↑n.succ) a
• AddGroupWithOne.intCast_negSucc 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [self : AddGroupWithOne R] (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• AddCommGroupWithOne.intCast_negSucc 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• AddCommGroupWithOne.mk 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [toAddCommGroup : AddCommGroup R] [toIntCast : IntCast R] [toNatCast : NatCast R] [toOne : One R] (natCast_zero : ↑0 = 0 := by intros; rfl) (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 := by intros; rfl) (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : AddCommGroupWithOne R
• AddGroupWithOne.mk 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [toIntCast : IntCast R] [toAddMonoidWithOne : AddMonoidWithOne R] [toNeg : Neg R] [toSub : Sub R] (sub_eq_add_neg : ∀ (a b : R), a - b = a + -b := by intros; rfl) (zsmul : ℤ → R → R) (zsmul_zero' : ∀ (a : R), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) (neg_add_cancel : ∀ (a : R), -a + a = 0) (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : AddGroupWithOne R
• Ring.zsmul_neg' 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [self : Ring R] (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• Ring.intCast_negSucc 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [self : Ring R] (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• NonAssocRing.intCast_negSucc 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• NonAssocRing.mk 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] [toOne : One α] (one_mul : ∀ (a : α), 1 * a = a) (mul_one : ∀ (a : α), a * 1 = a) [toNatCast : NatCast α] (natCast_zero : ↑0 = 0 := by intros; rfl) (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 := by intros; rfl) [toIntCast : IntCast α] (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : NonAssocRing α
• Ring.mk 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [toSemiring : Semiring R] [toNeg : Neg R] [toSub : Sub R] (sub_eq_add_neg : ∀ (a b : R), a - b = a + -b := by intros; rfl) (zsmul : ℤ → R → R) (zsmul_zero' : ∀ (a : R), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) (neg_add_cancel : ∀ (a : R), -a + a = 0) [toIntCast : IntCast R] (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : Ring R
• Int.cast_negSucc 📋 Mathlib.Data.Int.Cast.Basic
  {R : Type u} [AddGroupWithOne R] (n : ℕ) : ↑(Int.negSucc n) = -↑(n + 1)
• LinearOrderedAddCommGroupWithTop.zsmul_neg' 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (n : ℕ) (a : α) : LinearOrderedAddCommGroupWithTop.zsmul (Int.negSucc n) a = -LinearOrderedAddCommGroupWithTop.zsmul (↑n.succ) a
• LinearOrderedAddCommGroupWithTop.mk 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [toLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop α] [toNeg : Neg α] [toSub : Sub α] (sub_eq_add_neg : ∀ (a b : α), a - b = a + -b := by intros; rfl) (zsmul : ℤ → α → α) (zsmul_zero' : ∀ (a : α), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : α), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : α), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) [toNontrivial : Nontrivial α] (neg_top : -⊤ = ⊤) (add_neg_cancel_of_ne_top : ∀ ⦃x : α⦄, x ≠ ⊤ → x + -x = 0) : LinearOrderedAddCommGroupWithTop α
• LinearOrderedCommGroupWithZero.zpow_neg' 📋 Mathlib.Algebra.Order.GroupWithZero.Canonical
  {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (n : ℕ) (a : α) : LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑n.succ) a)⁻¹
• LinearOrderedCommGroupWithZero.mk 📋 Mathlib.Algebra.Order.GroupWithZero.Canonical
  {α : Type u_3} [toLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero α] [toInv : Inv α] [toDiv : Div α] (div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → α → α) (zpow_zero' : ∀ (a : α), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : α), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : α), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial α] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1) : LinearOrderedCommGroupWithZero α
• DivisionRing.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : DivisionRing K] (n : ℕ) (a : K) : DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
• DivisionSemiring.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : DivisionSemiring K] (n : ℕ) (a : K) : DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑n.succ) a)⁻¹
• Field.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u} [self : Field K] (n : ℕ) (a : K) : Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• Semifield.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : Semifield K] (n : ℕ) (a : K) : Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑n.succ) a)⁻¹
• DivisionSemiring.mk 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [toSemiring : Semiring K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → K → K) (zpow_zero' : ∀ (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial K] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) [toNNRatCast : NNRatCast K] (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den := by intros; rfl) (nnqsmul : ℚ≥0 → K → K) (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a := by intros; rfl) : DivisionSemiring K
• Semifield.mk 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [toCommSemiring : CommSemiring K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → K → K) (zpow_zero' : ∀ (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial K] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) [toNNRatCast : NNRatCast K] (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den := by intros; rfl) (nnqsmul : ℚ≥0 → K → K) (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a := by intros; rfl) : Semifield K
• DivisionRing.mk 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [toRing : Ring K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → K → K) (zpow_zero' : ∀ (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial K] [toNNRatCast : NNRatCast K] [toRatCast : RatCast K] (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) (inv_zero : 0⁻¹ = 0) (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den := by intros; rfl) (nnqsmul : ℚ≥0 → K → K) (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a := by intros; rfl) (ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den := by intros; rfl) (qsmul : ℚ → K → K) (qsmul_def : ∀ (a : ℚ) (x : K), qsmul a x = ↑a * x := by intros; rfl) : DivisionRing K
• Field.mk 📋 Mathlib.Algebra.Field.Defs
  {K : Type u} [toCommRing : CommRing K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → K → K) (zpow_zero' : ∀ (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial K] [toNNRatCast : NNRatCast K] [toRatCast : RatCast K] (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) (inv_zero : 0⁻¹ = 0) (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den := by intros; rfl) (nnqsmul : ℚ≥0 → K → K) (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a := by intros; rfl) (ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den := by intros; rfl) (qsmul : ℚ → K → K) (qsmul_def : ∀ (a : ℚ) (x : K), qsmul a x = ↑a * x := by intros; rfl) : Field K
• Int.negOfNat.eq_2 📋 Mathlib.Tactic.Ring.Basic
  (m : ℕ) : Int.negOfNat m.succ = Int.negSucc m
• Int.divisorsAntidiag.eq_2 📋 Mathlib.NumberTheory.Divisors
  (n : ℕ) : (Int.negSucc n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) (n + 1).divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding) (n + 1).divisorsAntidiagonal) ⋯
• DirectSum.GRing.intCast_negSucc_ofNat 📋 Mathlib.Algebra.DirectSum.Ring
  {ι : Type u_1} {A : ι → Type u_2} {inst✝ : AddMonoid ι} {inst✝¹ : (i : ι) → AddCommGroup (A i)} [self : DirectSum.GRing A] (n : ℕ) : DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)
• DirectSum.GRing.mk 📋 Mathlib.Algebra.DirectSum.Ring
  {ι : Type u_1} {A : ι → Type u_2} [AddMonoid ι] [(i : ι) → AddCommGroup (A i)] [toGSemiring : DirectSum.GSemiring A] (intCast : ℤ → A 0) (intCast_ofNat : ∀ (n : ℕ), intCast ↑n = DirectSum.GSemiring.natCast n) (intCast_negSucc_ofNat : ∀ (n : ℕ), intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)) : DirectSum.GRing A
• CochainComplex.ConnectData.X_negSucc 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (n : ℕ) : CochainComplex.ConnectData.X K L (Int.negSucc n) = K.X n
• CochainComplex.ConnectData.d.eq_3 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) : h.d (Int.negSucc 0) (Int.ofNat 0) = h.d₀
• CochainComplex.ConnectData.d.eq_2 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ) : h.d (Int.negSucc n) (Int.negSucc m) = K.d n m
• CochainComplex.ConnectData.d_negSucc 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ) : h.d (Int.negSucc n) (Int.negSucc m) = K.d n m
• CochainComplex.ConnectData.d.eq_4 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (a a_1 : ℕ) : h.d (Int.ofNat a) (Int.negSucc a_1) = 0
• CochainComplex.ConnectData.d.eq_5 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (a a_1 : ℕ) (x_2 : a = 0 → a_1 = 0 → False) : h.d (Int.negSucc a) (Int.ofNat a_1) = 0
• CochainComplex.ConnectData.restrictionLEIso_hom_f 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ) : h.restrictionLEIso.hom.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom
• CochainComplex.ConnectData.restrictionLEIso_inv_f 📋 Mathlib.Algebra.Homology.Embedding.Connect
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ) : h.restrictionLEIso.inv.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv
• Polynomial.Chebyshev.T.induct 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (motive : ℤ → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (Int.ofNat n.succ.succ)) (case4 : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (Int.negSucc n)) (a✝ : ℤ) : motive a✝
• Polynomial.Chebyshev.C.eq_4 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.C R (Int.negSucc n) = Polynomial.X * Polynomial.Chebyshev.C R (-↑n) - Polynomial.Chebyshev.C R (-↑n + 1)
• Polynomial.Chebyshev.S.eq_4 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.S R (Int.negSucc n) = Polynomial.X * Polynomial.Chebyshev.S R (-↑n) - Polynomial.Chebyshev.S R (-↑n + 1)
• Polynomial.Chebyshev.T.eq_4 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.T R (Int.negSucc n) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (-↑n) - Polynomial.Chebyshev.T R (-↑n + 1)
• Polynomial.Chebyshev.U.eq_4 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.U R (Int.negSucc n) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (-↑n) - Polynomial.Chebyshev.U R (-↑n + 1)
• zsmulRec.eq_2 📋 Mathlib.Topology.ContinuousMap.Bounded.Normed
  {G : Type u_1} [Zero G] [Add G] [Neg G] (nsmul : ℕ → G → G) (x✝ : G) (n : ℕ) : zsmulRec nsmul (Int.negSucc n) x✝ = -nsmul n.succ x✝
• Int.castDef.eq_2 📋 Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
  {R : Type u} [NatCast R] [Neg R] (n : ℕ) : (Int.negSucc n).castDef = -↑(n + 1)
• Turing.Tape.nth.eq_3 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} [Inhabited Γ] (T : Turing.Tape Γ) (n : ℕ) : T.nth (Int.negSucc n) = T.left.nth n
• Int.lnot.eq_1 📋 Mathlib.Data.Int.Bitwise
  (n : ℕ) : (Int.ofNat n).lnot = Int.negSucc n
• Int.bodd.eq_2 📋 Mathlib.Data.Int.Bitwise
  (n : ℕ) : (Int.negSucc n).bodd = !n.bodd
• Int.lnot.eq_2 📋 Mathlib.Data.Int.Bitwise
  (n : ℕ) : (Int.negSucc n).lnot = ↑n
• Int.bit_negSucc 📋 Mathlib.Data.Int.Bitwise
  (b : Bool) (n : ℕ) : Int.bit b (Int.negSucc n) = Int.negSucc (Nat.bit (!b) n)
• Int.lor.eq_2 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.ofNat m).lor (Int.negSucc n) = Int.negSucc (n.ldiff m)
• Int.lor.eq_3 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).lor (Int.ofNat n) = Int.negSucc (m.ldiff n)
• Int.ldiff.eq_4 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).ldiff (Int.negSucc n) = ↑(n.ldiff m)
• Int.ldiff.eq_3 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).ldiff (Int.ofNat n) = Int.negSucc (m ||| n)
• Int.lor.eq_4 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).lor (Int.negSucc n) = Int.negSucc (m &&& n)
• Int.xor.eq_2 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.ofNat m).xor (Int.negSucc n) = Int.negSucc (m ^^^ n)
• Int.xor.eq_3 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).xor (Int.ofNat n) = Int.negSucc (m ^^^ n)
• Int.ldiff.eq_2 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.ofNat m).ldiff (Int.negSucc n) = ↑(m &&& n)
• Int.xor.eq_4 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : (Int.negSucc m).xor (Int.negSucc n) = ↑(m ^^^ n)
• Int.shiftLeft_negSucc 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : Int.negSucc m <<< ↑n = Int.negSucc (Nat.shiftLeft' true m n)
• Int.bitwise.eq_2 📋 Mathlib.Data.Int.Bitwise
  (f : Bool → Bool → Bool) (m n : ℕ) : Int.bitwise f (Int.ofNat m) (Int.negSucc n) = Int.natBitwise (fun x y => f x !y) m n
• Int.bitwise.eq_3 📋 Mathlib.Data.Int.Bitwise
  (f : Bool → Bool → Bool) (m n : ℕ) : Int.bitwise f (Int.negSucc m) (Int.ofNat n) = Int.natBitwise (fun x y => f (!x) y) m n
• Int.bitwise.eq_4 📋 Mathlib.Data.Int.Bitwise
  (f : Bool → Bool → Bool) (m n : ℕ) : Int.bitwise f (Int.negSucc m) (Int.negSucc n) = Int.natBitwise (fun x y => f (!x) !y) m n
• Int.shiftRight_negSucc 📋 Mathlib.Data.Int.Bitwise
  (m n : ℕ) : Int.negSucc m >>> ↑n = Int.negSucc (m >>> n)
• Int.natBitwise.eq_1 📋 Mathlib.Data.Int.Bitwise
  (f : Bool → Bool → Bool) (m n : ℕ) : Int.natBitwise f m n = bif f false false then Int.negSucc (Nat.bitwise (fun x y => !f x y) m n) else ↑(Nat.bitwise f m n)
• ZNum.ofInt'.eq_2 📋 Mathlib.Data.Num.ZNum
  (n : ℕ) : ZNum.ofInt' (Int.negSucc n) = (Num.ofNat' (n + 1)).toZNumNeg
• Zsqrtd.Nonnegg.eq_4 📋 Mathlib.NumberTheory.Zsqrtd.Basic
  (c d a a_1 : ℕ) : Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = False
• Zsqrtd.Nonnegg.eq_2 📋 Mathlib.NumberTheory.Zsqrtd.Basic
  (c d a b : ℕ) : Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.negSucc b) = Zsqrtd.SqLe (b + 1) c a d
• Zsqrtd.Nonnegg.eq_3 📋 Mathlib.NumberTheory.Zsqrtd.Basic
  (c d a b : ℕ) : Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.ofNat b) = Zsqrtd.SqLe (a + 1) d b c
• HurwitzKernelBounds.f_int_negSucc 📋 Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
  (k : ℕ) {a : ℝ} (ha : a ≤ 1) (t : ℝ) (n : ℕ) : HurwitzKernelBounds.f_int k a t (Int.negSucc n) = HurwitzKernelBounds.f_nat k (1 - a) t n

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 519f454