Try new def for sub_vtx_ref.

Rename LagP_nodes -> LagP_node.

Fix dependencies.

Remove empty geom_simplex.

Extract node stuff from geom_simplex to new LagP_nodes.

  Finite_dim_AS_aff_span + Finite_dim_AS_aff_gen
  + Finite_dim_AS_Aff_indep + Finite_dim_AS_basis.
Update doc.
Update imports.

  + Finite_dim_MS_lin_map_R + Finite_dim_MS_duality + Finite_dim_AS_rest_R.
Add export modules Finite_dim_MS and Finite_dim_AS.
Update doc (used logic axioms + usage).
Update imports.

Update imports.

Mv FD_rest -> Finite_dim_MS_lin_map.

      has_dim into basis.
Update doc (used logic axioms).
Update imports.

  + AffineSpace_baryc + AffineSpace_aff_map + AffineSpace_sub.
Update doc (used logic axioms + usage).

  + ModuleSpace_lin_comb + ModuleSpace_lin_map + ModuleSpace_sub.
Update doc (usage).
Update imports.

  Ring_morphism + Ring_sub.
Add export module Ring.
Update doc (used logic axioms + usage).
Update imports.

Add export module Group.
Update doc (used logic axioms + usage).
Update imports.

  Monoid_morphism + Monoid_sum + Monoid_sub + ConcatnF + Monomial_order.

Add scope MonoidMult_scope.

       Bochner -> Bochner_wDep (= with deps).
Extract Lebesgue_p from Lebesgue_p_wDep (without deps),
        Bochner from Bochner_wDep (without deps).
Update imports.

Extract Algebra from Algebra_wDep (without deps).
Update imports.

Extract Subsets from Subsets_wDep (without deps).
Update imports.

Add export module numbers.

Rm compose (use comp from SSR),
   compose_assoc (use comp_assoc).
Rename Subset.swap -> Subset.swap_c,
       *compose* -> *comp*,
       {,pre}image_cancel -> {,pre}image_can,
Update imports.