Dealing with imports

Stream: new members

[Icaro Costa]

I am having problems dealing with imports in lean. When I do something like

import Mathlib

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) :=
sorry

The console says that range is an unknown identifier and I have no idea what to import to fix this.

[Rémy Degenne]

The full name of range is Finset.range. If you want to be able to omit the Finset namespace, you should open that namespace: put open Finset above your example.

[Rémy Degenne]

import Mathlib

open Finset

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) :=
  sorry

[Icaro Costa]

Rémy Degenne said:

The full name of range is Finset.range. If you want to be able to omit the Finset namespace, you should open that namespace: put open Finset above your example.

Thank you, that worked. I have two follow up questions:

• What's the difference between open and import?
• How can I look for libraries that I need for my theorem?

[Notification Bot]

This topic was moved here from #lean4 > Dealing with imports by Patrick Massot.

[Patrick Massot]

@Icaro Costa and @Rémy Degenne I moved this conversation to a better channel

[Rémy Degenne]

The top of that page explains imports and namespaces: https://lean-lang.org/theorem_proving_in_lean4/interacting_with_lean.html