Proving · 8 min

Libraries and mathematical notation

import loads a module; open shortens names from a namespace. A declaration such as Nat.gcd_comm is an existing theorem that you can apply directly. #check Nat.gcd_comm displays its full type and parameters.

Init is Lean’s core library. Std adds programming tools, including maps and sets. Mathlib is a separate community mathematics library with definitions and theorems for algebra, number theory, geometry, and analysis. This browser currently includes Init, so import Mathlib and tactics such as norm_num are unavailable.

Mathlib code often uses ℕ, ℤ, ℚ, ℝ, and ℂ for natural, integer, rational, real, and complex numbers. Other common notation includes ∑ for a finite sum, ∏ for a finite product, ∫ for an integral, √ for a square root, ∪ for union, ∩ for intersection, and ⊆ for subset. The required imports, types, and opened notation scopes determine how these expressions are interpreted.

In declarations such as variable (R : Type*) [CommRing R], the square brackets request an instance giving R its ring operations and laws. In x : ℝ, the colon still means “has type.” Writing a symbol or inserting its editor completion does not load the library that defines it.

Exercise

Prove that swapping the arguments of Nat.gcd leaves the result unchanged by applying Nat.gcd_comm.

import Init.Data.Nat.Gcd

theorem gcd_swap (a b : Nat) : Nat.gcd a b = Nat.gcd b a := by
  sorry

import Init.Data.Nat.Gcd

theorem gcd_swap (a b : Nat) : Nat.gcd a b = Nat.gcd b a := by
  exact Nat.gcd_comm a b

Related example