The New Coq Benchmarks

Library LinAlg.extras.Equality_structures

Library LinAlg.extras.matrix_algebra

Library LinAlg.extras.before_after

Library LinAlg.extras.Matrix_related_defs

Library LinAlg.extras.restrict

Library LinAlg.extras.finite_misc

Library LinAlg.extras.Inter_intersection

Library LinAlg.extras.ring_module

Library LinAlg.examples.Matrix_multiplication

Library LinAlg.examples.trivial_spaces

Library LinAlg.LinAlg.Lin_trafos

Lin_trafos.v

Library LinAlg.LinAlg.Linear_Algebra_by_Friedberg_Insel_Spence

Linear_Algebra_by_Friedberg_Insel_Spence.v

Library LinAlg.LinAlg.subspace_bases

subspace_bases.v

Library LinAlg.LinAlg.subspace_dim

subspace_dim.v

Library LinAlg.LinAlg.maxlinindepsubsets

maxlinindepsubsets.v

Library LinAlg.LinAlg.bases_finite_dim

bases_finite_dim.v

Library LinAlg.LinAlg.replacement_corollaries

replacement_corollaries.v

Library LinAlg.LinAlg.replacement_theorem

replacement_theorem.v

Library LinAlg.LinAlg.bases_from_generating_sets

bases_from_generating_sets.v

Library LinAlg.LinAlg.bases

bases.v

Library LinAlg.support.counting_elements

Library LinAlg.support.has_n_elements

Library LinAlg.support.finite_subsets

Library LinAlg.support.random_facts

Library LinAlg.LinAlg.lin_dep_facts

lin_dep_facts.v

Library LinAlg.LinAlg.lin_dependence

lin_dependence.v

Library LinAlg.LinAlg.direct_sum

direct_sum.v

Library LinAlg.LinAlg.lin_comb_facts

lin_comb_facts.v

Library LinAlg.LinAlg.algebraic_span_facts

algebraic_span_facts.v

Library LinAlg.LinAlg.spans

spans.v

Library LinAlg.LinAlg.lin_combinations

lin_combinations.v

Library LinAlg.support.cast_between_subsets

Library LinAlg.support.distinct_facts

Library LinAlg.support.omit_facts

Library LinAlg.support.seq_set_facts

Library LinAlg.support.distribution_lemmas

Library LinAlg.support.seq_equality_facts

Library LinAlg.support.concat_facts

Library LinAlg.support.seq_equality

Library LinAlg.support.cast_seq_lengths

Library LinAlg.support.distinct

Library LinAlg.support.sums2

Library LinAlg.support.sums

Library LinAlg.support.subseqs

Library LinAlg.support.Map_embed

Library LinAlg.support.mult_by_scalars

Library LinAlg.support.modify_seq

Library LinAlg.support.pointwise

Library LinAlg.support.omit

Library LinAlg.support.const

Library LinAlg.support.concat

Library LinAlg.support.conshdtl

Library LinAlg.support.empty

Library LinAlg.support.seq_set_seq

Library LinAlg.support.seq_set

Library LinAlg.examples.up_lo_triang_mat

Library LinAlg.examples.symmetric_matrices

Library LinAlg.examples.antisymmetric_matrices

Library LinAlg.LinAlg.subspaces

subspaces.v

Library LinAlg.support.arb_intersections

Library LinAlg.support.algebra_omissions

Library LinAlg.examples.infinite_sequences

Library LinAlg.LinAlg.alt_build_vecsp

alt_build_vecsp.v

Library LinAlg.examples.vecspace_Mmn

Library LinAlg.examples.Matrices

Library LinAlg.examples.vecspace_functionspace

Library LinAlg.support.Map2

Library LinAlg.examples.vecspace_Fn

Library LinAlg.support.finite

Library LinAlg.LinAlg.vecspaces_verybasic

vecspaces_verybasic.v

Library LinAlg.support.more_syntax

Library LinAlg.support.equal_syntax

Library LinAlg.first_page