Zulip Chat Archive

Stream: kbb

Topic: fin cases bashing


view this post on Zulip Johan Commelin (Sep 18 2018 at 12:22):

@Scott Morrison Could your tactic also expand things like (↑(finset.sum finset.univ (λ (j : fin 2), A 0 j * B j 1))? I would like to write expand_fin; ring as proof of a goal I'm currently having... (working with 2x2 matrices)


Last updated: May 18 2021 at 10:14 UTC