Diffusion afp-devel db93f67adfd0

generalized theory name: euclidean division denotes one particular division…
db93f67adfd0
Actions

Description

generalized theory name: euclidean division denotes one particular division definition on integers

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP75e99d0e6664: more efficient specification

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….Jan 24 2023, 11:31 AM

Fabian Huch <huch@in.tum.de> mentioned this in rAFP48cd0dd582dd: adapted to db93f67a;.Jan 24 2023, 5:57 PM

Changes (41)

Path

Size

thys/

BenOr_Kozen_Reif/

More_Matrix.thy

Berlekamp_Zassenhaus/

Berlekamp_Type_Based.thy

Finite_Field_Factorization_Record_Based.thy

Finite_Field_Record_Based.thy

CRYSTALS-Kyber/

Compress.thy

NTT_Scheme.thy

DPRM_Theorem/

Machine_Equations/

Machine_Equation_Equivalence.thy

Register_Machine/

MachineMasking.thy

MultipleToSingleSteps.thy

Design_Theory/

Resolvable_Designs.thy

Dict_Construction/

Test_Lazy_Case.thy

Digit_Expansions/

Bits_Digits.thy

Finite_Fields/

Ring_Characteristic.thy

Finitely_Generated_Abelian_Groups/

Finitely_Generated_Abelian_Groups.thy

Formula_Derivatives/

Presburger_Formula.thy

IMP2/

doc/

Examples.thy

Modular_arithmetic_LLL_and_HNF_algorithms/

Signed_Modulo.thy

Storjohann.thy

Multi_Party_Computation/

ETP_RSA_OT.thy

Number_Theoretic_Transform/

Butterfly.thy

Preliminary_Lemmas.thy

Padic_Field/

Padic_Field_Powers.thy

Padic_Ints/

Padic_Integers.thy

Polynomial_Factorization/

Prime_Factorization.thy

Polynomial_Interpolation/

Improved_Code_Equations.thy

Projective_Measurements/

Linear_Algebra_Complements.thy

Registers/

Finite_Tensor_Product_Matrices.thy

Sigma_Commit_Crypto/

Rivest.thy

Schnorr_Sigma_Commit.thy

Solidity/

Constant_Folding.thy

ReadShow.thy

Subresultants/

Binary_Exponentiation.thy

Dichotomous_Lazard.thy

Van_Emde_Boas_Trees/

VEBT_Definitions.thy

VEBT_Delete.thy

VEBT_DeleteCorrectness.thy

VEBT_Insert.thy

VEBT_InsertCorrectness.thy

VEBT_Member.thy

VEBT_MinMax.thy

Word_Lib/

More_Word_Operations.thy

rAFPdb93f67adfd0

View Options

thys/BenOr_Kozen_Reif/More_Matrix.thy

View Options

thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy

View Options

thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy

View Options

thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy

View Options

thys/CRYSTALS-Kyber/Compress.thy

View Options

thys/CRYSTALS-Kyber/NTT_Scheme.thy

View Options

thys/DPRM_Theorem/Machine_Equations/Machine_Equation_Equivalence.thy

View Options

thys/DPRM_Theorem/Register_Machine/MachineMasking.thy

View Options

thys/DPRM_Theorem/Register_Machine/MultipleToSingleSteps.thy

View Options

thys/Design_Theory/Resolvable_Designs.thy

View Options

thys/Dict_Construction/Test_Lazy_Case.thy

View Options

thys/Digit_Expansions/Bits_Digits.thy

View Options

thys/Finite_Fields/Ring_Characteristic.thy

View Options

thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy

View Options

thys/Formula_Derivatives/Presburger_Formula.thy

View Options

thys/IMP2/doc/Examples.thy

View Options

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Signed_Modulo.thy

View Options

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy

View Options

thys/Multi_Party_Computation/ETP_RSA_OT.thy

View Options

thys/Number_Theoretic_Transform/Butterfly.thy

View Options

thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy

View Options

thys/Padic_Field/Padic_Field_Powers.thy

View Options

thys/Padic_Ints/Padic_Integers.thy

View Options

thys/Polynomial_Factorization/Prime_Factorization.thy

View Options

thys/Polynomial_Interpolation/Improved_Code_Equations.thy

View Options

thys/Projective_Measurements/Linear_Algebra_Complements.thy

View Options

thys/Registers/Finite_Tensor_Product_Matrices.thy

View Options

thys/Sigma_Commit_Crypto/Rivest.thy

View Options

thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy

View Options

thys/Solidity/Constant_Folding.thy

View Options

thys/Solidity/ReadShow.thy

View Options

thys/Subresultants/Binary_Exponentiation.thy

View Options

thys/Subresultants/Dichotomous_Lazard.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_Definitions.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_Delete.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_DeleteCorrectness.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_Insert.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_Member.thy

View Options

thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy

View Options

thys/Word_Lib/More_Word_Operations.thy

generalized theory name: euclidean division denotes one particular division…db93f67adfd0Actions

Description

Details

Event Timeline

Changes (41)

rAFPdb93f67adfd0

thys/BenOr_Kozen_Reif/More_Matrix.thy

thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy

thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy

thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy

thys/CRYSTALS-Kyber/Compress.thy

thys/CRYSTALS-Kyber/NTT_Scheme.thy

thys/DPRM_Theorem/Machine_Equations/Machine_Equation_Equivalence.thy

thys/DPRM_Theorem/Register_Machine/MachineMasking.thy

thys/DPRM_Theorem/Register_Machine/MultipleToSingleSteps.thy

thys/Design_Theory/Resolvable_Designs.thy

thys/Dict_Construction/Test_Lazy_Case.thy

thys/Digit_Expansions/Bits_Digits.thy

thys/Finite_Fields/Ring_Characteristic.thy

thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy

thys/Formula_Derivatives/Presburger_Formula.thy

thys/IMP2/doc/Examples.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Signed_Modulo.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy

thys/Multi_Party_Computation/ETP_RSA_OT.thy

thys/Number_Theoretic_Transform/Butterfly.thy

thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy

thys/Padic_Field/Padic_Field_Powers.thy

thys/Padic_Ints/Padic_Integers.thy

thys/Polynomial_Factorization/Prime_Factorization.thy

thys/Polynomial_Interpolation/Improved_Code_Equations.thy

thys/Projective_Measurements/Linear_Algebra_Complements.thy

thys/Registers/Finite_Tensor_Product_Matrices.thy

thys/Sigma_Commit_Crypto/Rivest.thy

thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy

thys/Solidity/Constant_Folding.thy

thys/Solidity/ReadShow.thy

thys/Subresultants/Binary_Exponentiation.thy

thys/Subresultants/Dichotomous_Lazard.thy

thys/Van_Emde_Boas_Trees/VEBT_Definitions.thy

thys/Van_Emde_Boas_Trees/VEBT_Delete.thy

thys/Van_Emde_Boas_Trees/VEBT_DeleteCorrectness.thy

thys/Van_Emde_Boas_Trees/VEBT_Insert.thy

thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy

thys/Van_Emde_Boas_Trees/VEBT_Member.thy

thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy

thys/Word_Lib/More_Word_Operations.thy

generalized theory name: euclidean division denotes one particular division…
db93f67adfd0
Actions