Batteries references

Every Batteries declaration referred to directly by this project’s own code, grouped by the module it comes from.

definition theorem
legend

Classes.RatCast

Canonical homomorphism from Rat to a division ring K. This is just the bare function in order to aid in creating instances of DivisionRing.

def Rat.cast.{u} {K : Type u} [RatCast K] : ℚ → K

Used by: irrational_logb_two_five, irrational_logb_two_three

Data.List.Basic

Forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

inductive List.Forall₂.{u_1, u_2} {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : List α → List β → Prop

Used by: Logic.Popper.Basis1.forall₂_mutual_refl, Logic.Popper.Basis1.substitutivity

IsChain R l means that R holds between adjacent elements of l. Example:

IsChain R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
inductive List.IsChain.{u_1} {α : Type u_1} (R : α → α → Prop) : List α → Prop

Used by: InformationSystem.Chain.ofIsChain, InformationSystem.Run

theorem List.isChain_cons_cons.{u_1} {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} :
  List.IsChain R (a :: b :: l) ↔ R a b ∧ List.IsChain R (b :: l)

Used by: InformationSystem.Chain.ofIsChain

Data.List.Lemmas

theorem List.nodup_finRange (n : ℕ) : (List.finRange n).Nodup

Used by: Logic.PropositionalLogic.Formula.completeness

Logic

theorem eq_rec_constant.{u_1, u_2} {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a') : h ▸ y = y

Used by: Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex