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

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.Run

Data.List.Lemmas

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

Used by: Propositional.Formula.completeness