Zulip Chat Archive
Stream: general
Topic: rewrite rule
Joseph O (Nov 05 2022 at 16:50):
How can i rewrite n(n-1)/2=sum n as n(n-1)=2*(sum n) in a lean proof
Andrew Yang (Nov 05 2022 at 16:53):
It is usually docs#div_eq_iff but I cannot be sure unless there is an #mwe.
Joseph O (Nov 05 2022 at 17:08):
what namespace is it under, bc it can't find it
Kyle Miller (Nov 05 2022 at 17:10):
It's in the top-level namespace, but to use it you need to import algebra.group_with_zero.units (or import something that imports this module).
Joseph O (Nov 05 2022 at 17:10):
Thank you.
Kyle Miller (Nov 05 2022 at 17:11):
The module name is the top-middle of the docs page that Andrew gave
Last updated: Dec 20 2023 at 11:08 UTC