filesInOrder

first_page.v

support/equal_syntax.v
support/more_syntax.v
LinAlg/vecspaces_verybasic.v

support/finite.v
examples/vecspace_Fn.v

support/Map2.v
examples/vecspace_functionspace.v
examples/Matrices.v
examples/vecspace_Mmn.v

LinAlg/alt_build_vecsp.v
examples/infinite_sequences.v

support/algebra_omissions.v
support/arb_intersections.v
LinAlg/subspaces.v

examples/antisymmetric_matrices.v
examples/symmetric_matrices.v
examples/up_lo_triang_mat.v

support/seq_set.v
support/seq_set_seq.v
support/empty.v
support/conshdtl.v
support/concat.v
support/const.v
support/omit.v
support/pointwise.v
support/modify_seq.v
support/mult_by_scalars.v
support/Map_embed.v
support/subseqs.v
support/sums.v
support/sums2.v
support/distinct.v
support/cast_seq_lengths.v
support/seq_equality.v
support/concat_facts.v
support/seq_equality_facts.v
support/distribution_lemmas.v
support/seq_set_facts.v
support/omit_facts.v
support/distinct_facts.v

support/cast_between_subsets.v

LinAlg/lin_combinations.v
LinAlg/spans.v
LinAlg/algebraic_span_facts.v
LinAlg/lin_comb_facts.v
LinAlg/direct_sum.v
LinAlg/lin_dependence.v
LinAlg/lin_dep_facts.v

support/random_facts.v
support/finite_subsets.v
support/has_n_elements.v
support/counting_elements.v
LinAlg/bases.v
LinAlg/bases_from_generating_sets.v
LinAlg/replacement_theorem.v
LinAlg/replacement_corollaries.v
LinAlg/bases_finite_dim.v
LinAlg/maxlinindepsubsets.v
LinAlg/subspace_dim.v
LinAlg/subspace_bases.v
LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v
LinAlg/Lin_trafos.v

examples/trivial_spaces.v
examples/Matrix_multiplication.v

extras/ring_module.v
extras/Inter_intersection.v
extras/finite_misc.v
extras/restrict.v
extras/Matrix_related_defs.v
extras/before_after.v
extras/matrix_algebra.v
extras/Equality_structures.v