i seem to have no access to mathlib...

Stream: new members

[Lawrence Lin]

i'm following all the steps on https://leanprover-community.github.io/install/windows.html correctly but lean doesn't seem to know where i have mathlib installed. in particular, I can't do

import geom_sum

without lean getting mad.

[Lawrence Lin]

nvm, resolved. i do have mathlib installed, i just don't know how to get it to access geom_sum.

[Anne Baanen]

It looks like you fixed your issue in another thread but for future reference: to access geom_sum lemmas, you should write import algebra.geom_sum.