leanprover-community/mathlib

Pull Requests Commits

feat(tactic/linter): add decidable_classical linter (#2352)

sgouezel committed 5 years ago

Verified 55d430ca

feat(data/support): define support of a function and prove some properties (#2340)

urkud committed 5 years ago

Verified 65a5dc0f

fix(tactic/solve_by_elim): fix metavariable bug from #2269 (#2289)

kim-em committed 5 years ago

Verified b550c165

feat(data/list/basic): some lemmas about sum/head/tail for list ℕ (#2342)

kim-em committed 5 years ago

Verified bd21cffc

feat (data/list/basic): lemmas about prod and take (#2345)

kim-em committed 5 years ago

Verified cb8d8ace

feat(data/list/basic): nth_le 0 = head (#2350)

kim-em committed 5 years ago

Verified 732f7109

feat(algebra/group/basic.lean): add inv_mul_eq_one (#2349)

kbuzzard committed 5 years ago

Verified 0e2970c7

feat(algebra/homology): functoriality of induced maps on cycles (#2338)

TwoFX committed 5 years ago

Verified 34ae62ad

chore(test/refine_struct): remove dead code (#2348)

gebner committed 5 years ago

Verified e2fa8b2b

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

abccc301

refactor(measure_theory/borel): `borel` is not an `instance` (#2326)

urkud committed 5 years ago

Verified 6f75c57e

feat(data/list/basic): add map_take/drop_take (#2344)

kim-em committed 5 years ago

Verified 97c43025

chore(data/list/basic): rename take_all -> take_length (#2343)

kim-em committed 5 years ago

Verified 2f2e016e

feat(data/real/nnreal): coe_max and coe_min (#2346)

jcommelin committed 5 years ago

Verified d936c288

fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id` (#2319)

urkud committed 5 years ago

Verified c85453d9

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

df64ea9c

chore(algebra/big_operators): drop some `decidable_eq` assumptions (#2332)

urkud committed 5 years ago

Verified 60d14579

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

7628c6c7

feat(algebra/group_with_zero): groups with a zero element adjoined (#2242)

jcommelin committed 5 years ago

Verified 48cc0c81

fix(data/finset): add comment (#2336)

kbuzzard committed 5 years ago

Verified 89fdec6e

feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (#2324)

shingtaklam1324 committed 5 years ago

Verified 7b120a35

feat(topology/bounded_continuous_function): composition of limits when uniform convergence (#2260)

sgouezel committed 5 years ago

Verified ff910dca

chore(topology/instances/ennreal): prove `tendsto_iff_edist_tendsto_0` (#2333)

urkud committed 5 years ago

Verified 572fad12

chore(algebra/field): move some lemmas from `field` to `division_ring` (#2331)

urkud committed 5 years ago

Verified 3d60e134

feat(order/filter): more eventually/frequently API (#2330)

PatrickMassot committed 5 years ago

Verified a2e76391

feat(logic/embedding): embedding punit/prod (#2315)

kim-em committed 5 years ago

Verified 26bf2730

feat(tactic/linarith): split conjunctions in hypotheses (#2320)

robertylewis committed 5 years ago

Verified 23681c3d

feat(*/multilinear): more material (#2197)

sgouezel committed 5 years ago

Verified dea8bd4b

chore(ci): always push release to azure (#2321)

bryangingechen committed 5 years ago

Verified 8406896b

feat(data/mv_polynomial): add partial derivatives (#2298)

shingtaklam1324 committed 5 years ago

Verified 63aa8b1e

Newer Older