Diffusion afp-devel 1b546d918c0c

Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various…
1b546d918c0c
Actions

Tags

None

Subscribers

None

Description

Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various small results required for upcoming commit.

Details

Provenance

Emin Karayel <me@eminkarayel.de>

Authored on

Parents

rAFP672eb4689f1a: merged

Branches

Unknown

Tags

Unknown

Event Timeline

Emin Karayel <me@eminkarayel.de> committed rAFP1b546d918c0c: Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various….Sat, Apr 20, 1:07 AM

Changes (6)

Path

Size

Concentration_Inequalities/

Concentration_Inequalities_Preliminary.thy

Find_Irreducible_Poly.thy

Finite_Fields_More_PMF.thy

Universal_Hash_Families/

Universal_Hash_Families_More_Independent_Families.thy

rAFP1b546d918c0c

thys/Concentration_Inequalities/Concentration_Inequalities_Preliminary.thy

Loading...

thys/Finite_Fields/Find_Irreducible_Poly.thy

Loading...

thys/Finite_Fields/Finite_Fields_More_PMF.thy

Loading...

thys/Universal_Hash_Families/Universal_Hash_Families_More_Independent_Families.thy

Loading...