Files

 main

/

Library.lean

Blame

Blame

Latest commit

 

History

History

26 lines (26 loc) · 828 Bytes

 main

/

Library.lean

Top

File metadata and controls

• Code
• Blame

26 lines (26 loc) · 828 Bytes

Raw

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

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.Define

import Library.Tactic.Define.Attr

import Library.Tactic.ExistsDelaborator

import Library.Tactic.Extra

import Library.Tactic.Extra.Attr

import Library.Tactic.FiniteInductive

import Library.Tactic.Induction

import Library.Tactic.ModCases

import Library.Tactic.Numbers

import Library.Tactic.Product

import Library.Tactic.Rel

import Library.Tactic.Rel.Attr

import Library.Tactic.Use

import Library.Tactic.TruthTable