Session Dirichlet_L
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Lattice_Algebras
HOL-Library.Interval
HOL-Library.Log_Nat
HOL-Library.Float
HOL-Library.Interval_Float
HOL-Decision_Procs.Dense_Linear_Order
File ‹langford_data.ML›
File ‹ferrante_rackoff_data.ML›
File ‹langford.ML›
File ‹ferrante_rackoff.ML›
HOL-Decision_Procs.Approximation_Bounds
Lehmer.Lehmer
Pratt_Certificate.Pratt_Certificate
File ‹pratt.ML›
Bertrands_Postulate.Bertrand
File ‹bertrand.ML›
Finitely_Generated_Abelian_Groups.Set_Multiplication
Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
HOL-Algebra.QuotRing
HOL-Algebra.IntRing
Finitely_Generated_Abelian_Groups.General_Auxiliary
Finitely_Generated_Abelian_Groups.IDirProds
Finitely_Generated_Abelian_Groups.Finite_Product_Extend
Finitely_Generated_Abelian_Groups.Group_Hom
Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
Finitely_Generated_Abelian_Groups.DirProds
Finitely_Generated_Abelian_Groups.Group_Relations
Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
Multiplicative_Characters
Dirichlet_Characters
Dirichlet_L_Functions
Dirichlet_Theorem