math2001/Library.lean at main · hrmacbeth/math2001 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
import Library.Basic
import Library.Config.Constructor
import Library.Config.Contradiction
import Library.Config.ExistsDelaborator
import Library.Config.Initialize
import Library.Config.Ring
import Library.Config.Set
import Library.Config.Use
import Library.Theory.Comparison
import Library.Theory.Division
import Library.Theory.InjectiveSurjective
import Library.Theory.GCD
import Library.Theory.ModEq.Defs
import Library.Theory.ModEq.Lemmas
import Library.Theory.NumberTheory
import Library.Theory.Parity
import Library.Theory.ParityModular
import Library.Theory.Prime
import Library.Tactic.Addarith
import Library.Tactic.Cancel
import Library.Tactic.Exhaust
import Library.Tactic.Extra.Attr
import Library.Tactic.Extra.Basic
import Library.Tactic.Extra.ModEq
import Library.Tactic.Induction
import Library.Tactic.ModCases
import Library.Tactic.ModEq
import Library.Tactic.Numbers.Basic
import Library.Tactic.Numbers.ModEq
import Library.Tactic.Obtain
import Library.Tactic.Rel
import Library.Tactic.Rel.Attr
import Library.Tactic.TruthTable