Stream: Beginner Questions

Topic: Generalizing some lemmas about vector spaces to modules

view this post on Zulip Yong Kiam (Nov 02 2023 at 09:31):

I ran into a slight annoyance with this lemma (and some similar ones): https://www.isa-afp.org/sessions/jordan_normal_form/#VS_Connect.html#VS_Connect.vec_space.finsum_index|fact

The problem was I needed it for int vec (working over modules). It was easy enough for me to copy-paste the proofs into vec_module instead of vec_space.

I'm wondering if anyone has done this systematically in another AFP entry or somewhere else?

Last updated: Nov 13 2025 at 04:27 UTC