Commit 2021-10-05 12:20 1dba5d4d

View on Github →

feat: List.product (#59)

Estimated changes

Modified .github/workflows/build.yml

Deleted GNUmakefile

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

added def List.product

added theorem List.product_spec

Modified Mathlib/Logic/Basic.lean

added theorem and_symm_left

added theorem and_symm_right

added theorem exists_eq_right_right'

added theorem exists_eq_right_right

added theorem exists_prop

Modified Mathlib/Tactic/Basic.lean

Modified Mathlib/Tactic/Ring.lean

Modified Mathlib/Tactic/RunTac.lean

Renamed test/Find.lean to Mathlib/Test/Find.lean

Renamed test/SolveByElim.lean to Mathlib/Test/SolveByElim.lean

Renamed test/Split.lean to Mathlib/Test/Split.lean

Deleted test/basicTactics.lean

Deleted test/ring.lean

Deleted test/runTac.lean

Deleted test/spread.lean