leanprover-community/mathlib

Pull Requests Commits

style(*): use rcases patterns with ext (#3018)

robertylewis committed 5 years ago

daed8a41

ci(build.yml): add -T100000 to test step (#3017)

bryangingechen committed 5 years ago

026d639f

chore(*): update to lean 3.16.0 (#3016)

gebner committed 5 years ago

614d1cad

chore(algebra/field): deduplicate with group_with_zero (#3015)

urkud committed 5 years ago

4b622613

chore(data/equiv/basic): add many docstrings, review (#3008)

urkud committed 5 years ago

b427ebf9

feat(control/equiv_functor/instances): allow equiv_rw on finset (#2997)

kim-em committed 5 years ago

671284e3

feat(data/set/function): add lemmas about `semiconj` (#3007)

urkud committed 5 years ago

b932a510

chore(*): use sum notation (#3014)

kckennylau committed 5 years ago

836c0a26

feat(linear_algebra/basic): curry is linear_equiv (#3012)

pechersky committed 5 years ago

d9934b26

chore(data/fintype): generalise `to_finset_card` (#2316)

kim-em committed 5 years ago

6a0412e9

feat(group_theory/subgroup): normal_closure and gpowers (#2959)

ChrisHughes24 committed 5 years ago

f1df14c2

chore(algebra/group_power): simp attribute on nsmul_eq_mul and gsmul_eq_mul (#2983)

sgouezel committed 5 years ago

4e1558bf

refactor(group_theory/subgroup): swap `mul_mem_cancel_left/right` (#3011)

urkud committed 5 years ago

a02ab48a

chore(scripts): update nolints.txt (#3010)

leanprover-community-bot committed 5 years ago

df34ee20

refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844)

jcommelin committed 5 years ago

1a4f0c22

feat(ring_theory/localization): more lemmas and defs about fields of fractions (#3005)

101damnations committed 5 years ago

f098c16e

feat(category_theory/limits): prod.lift_comp_comp (#2968)

TwoFX committed 5 years ago

ccdf1d27

refactor(topology): rename `lim` to `Lim` (#2977)

urkud committed 5 years ago

7cb0a851

feat(algebra/add_torsor): add `prod.add_torsor` (#2980)

urkud committed 5 years ago

76792dcc

refactor(data/polynomial): redefine `C` as an `alg_hom` (#3003)

urkud committed 5 years ago

42813431

chore(ring_theory/algebra): add comments explaining absence of 2 `simp` attrs (#3002)

urkud committed 5 years ago

34302c63

chore(data/real/nnreal): +2 lemmas (#3000)

urkud committed 5 years ago

03c345ff

feat(analysis/special_functions/pow): `inv_rpow`, `div_rpow` (#2999)

urkud committed 5 years ago

10914620

chore(algebra/big_operators): add `@[simp] lemma sum_eq_zero_iff` (#2998)

urkud committed 5 years ago

45567dcc

chore(data/matrix/basic): clean up of new lemmas on matrix numerals (#2996)

kim-em committed 5 years ago

24ce416a

feat(dynamics/fixed_points/topology): new file (#2991)

urkud committed 5 years ago

7bb2d89f

chore(scripts): update nolints.txt (#2993)

leanprover-community-bot committed 5 years ago

470ccd32

feat(data/real/conjugate_exponents): define real conjugate exponents (#2992)

sgouezel committed 5 years ago

94dedddf

chore(*): use prod notation (#2989)

kckennylau committed 5 years ago

4ee67acb

feat(geometry/euclidean): angles and some basic lemmas (#2865)

jsm28 committed 5 years ago

a377993a

Older