leanprover-community/mathlib3

Pull Requests Commits

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

feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma (#2850)

dwarn committed 5 years ago

dbbd696d

chore(*): add docs and nolints (#2990)

urkud committed 5 years ago

d204daa5

refactor(algebra/*): move `commute` below `ring` in `import`s (#2973)

urkud committed 5 years ago

9fba817f

feat(data/matrix/basic): add bit0, bit1 lemmas (#2987)

pechersky committed 5 years ago

2caf479d

chore(algebra/ordered_ring): use le instead of ge (#2986)

sgouezel committed 5 years ago

3ca4c270

feat(data/nat/digits): digits, and divisibility tests for Freek 85 (#2686)

kim-em committed 5 years ago

47f73356

Older