Theorem add_val

refactor(linear_algebra, ring_theory): rework submodules; move them to linear_algebra

fix(linear_algebra/subtype): simplify lifted operations by using projections instead of match

refactor(algebra/module): split of type constructions and move quotient, subtype and linear_map to their own theories in algebra/linear_algebra