feat(algebra): define `invertible` typeclass (#2504)
In the discussion for #2480, we decided that the definitions would be cleaner if the elaborator could supply us with a suitable value of `1/2`. With these changes, we can now add an `[invertible 2]` argument to write `⅟ 2`.
Related to Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232480.20bilinear.20forms
