CoCalc Public Filestmp / b.leanOpen in with one click!
Author: William A. Stein
1
import data.nat.dist -- distance function
2
3
import data.nat.gcd -- gcd
4
import data.nat.modeq -- modular arithmetic
5
import data.nat.prime -- prime number stuff
6
import data.nat.sqrt -- square roots
7
import tactic.norm_num -- a tactic for fast computations
8
9
open nat
10
11
12
example : fact 4 = 24 := rfl -- factorial
13
14
example (a : ) : fact a > 0 := fact_pos a