leanprover-community/mathlib3

Pull Requests Commits

fix(algebra/euclidean_domain): remove decidable_eq assumption (#2362)

gebner committed 6 years ago

Verified 80d3ed8f

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

67b121e4

chore(data/list): move some sections to separate files (#2341)

kim-em committed 6 years ago

Verified fbc95927

Bugfix for norm num when testing divisibility of integers (#2355)

alexjbest committed 6 years ago

Verified e4e483e5

feat(analysis/analytic/basic): change origin of power series (#2327)

sgouezel committed 6 years ago

Verified c3d9cf90

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

dae7154d

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

sgouezel committed 6 years ago

Verified 55d430ca

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

urkud committed 6 years ago

Verified 65a5dc0f

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

kim-em committed 6 years ago

Verified b550c165

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

kim-em committed 6 years ago

Verified bd21cffc

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

kim-em committed 6 years ago

Verified cb8d8ace

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

kim-em committed 6 years ago

Verified 732f7109

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

kbuzzard committed 6 years ago

Verified 0e2970c7

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

TwoFX committed 6 years ago

Verified 34ae62ad

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

gebner committed 6 years ago

Verified e2fa8b2b

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

abccc301

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

urkud committed 6 years ago

Verified 6f75c57e

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

kim-em committed 6 years ago

Verified 97c43025

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

kim-em committed 6 years ago

Verified 2f2e016e

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

jcommelin committed 6 years ago

Verified d936c288

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

urkud committed 6 years ago

Verified c85453d9

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

df64ea9c

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

urkud committed 6 years ago

Verified 60d14579

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

7628c6c7

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

jcommelin committed 6 years ago

Verified 48cc0c81

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

kbuzzard committed 6 years ago

Verified 89fdec6e

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

shingtaklam1324 committed 6 years ago

Verified 7b120a35

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

sgouezel committed 6 years ago

Verified ff910dca

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

urkud committed 6 years ago

Verified 572fad12

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

urkud committed 6 years ago

Verified 3d60e134

Newer Older