Explicit `is_submodule`

Stream: maths

[Chris Hughes]

What's the reason lemmas like span_eq_of_is_submodule in linear_algebra.basic take an explicit is_submodule argument, rather than using type class inference?