27 lines
829 BLFS
Lean4
27 lines
829 BLFS
Lean4
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
|