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: Aug 03 2023 at 10:10 UTC