Zulip Chat Archive

Stream: new members

Topic: i seem to have no access to mathlib...

Lawrence Lin (Nov 10 2022 at 03:03):

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 (Nov 10 2022 at 03:24):

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

Anne Baanen (Nov 10 2022 at 09:47):

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.

Last updated: Dec 20 2023 at 11:08 UTC