leanprover-community/mathlib

Pull Requests Commits

feat(analysis/special_functions): limit of x^s * exp(-x) for s real (#12540)

loefflerd committed 4 years ago

1326aa7c

refactor(algebra/group/to_additive): monadic code cosmetics (#12527)

nomeata committed 4 years ago

e553f8ad

feat(data/setoid/partition): Relate `setoid.is_partition` and `finpartition` (#12459)

AntoineChambert-Loir committed 4 years ago

47b1ddf2

fix(probability): remove unused argument from `cond_cond_eq_cond_inter` (#12583)

rish987 committed 4 years ago

115f8c7a

feat(data/nat/{nth,prime}): add facts about primes (#12560)

kmill committed 4 years ago

3061d18f

feat(group_theory/commutator): Add some basic lemmas (#12554)

tb65536 committed 4 years ago

de4d14cb

refactor(group_theory/commutator): Golf proof of `commutator_mem_commutator` (#12584)

tb65536 committed 4 years ago

355472dc

feat(data/list/basic): Lists over empty type are `unique` (#12582)

vihdzp committed 4 years ago

b5a26d0a

refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572)

tb65536 committed 4 years ago

f0dd6e9b

refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)

tb65536 committed 4 years ago

6c04fcf4

feat(algebra/group/to_additive + a few more files): make `to_additive` convert `unit` to `add_unit` (#12564)

adomani committed 4 years ago

84cbbc98

feat(data/zmod/basic): some lemmas about coercions (#12571)

eric-wieser committed 4 years ago

869ef84f

chore(*): clear up some excessive by statements (#12570)

alexjbest committed 4 years ago

6fdb1d5d

feat(field_theory/is_alg_closed/basic): add `is_alg_closed.infinite` (#12566)

Jlh18 committed 4 years ago

45c22c0d

feat(tactic/norm_num_command): add user command to run norm_num on an expression (#12550)

kmill committed 4 years ago

0e93816c

chore(*): remove lines claiming to introduce variables (#12569)

adomani committed 4 years ago

f654a86a

chore(order/galois_connection): Make lifting instances reducible (#12559)

YaelDillies committed 4 years ago

4a59a4d4

chore(cardinal_divisibility): tiny golf (#12567)

ericrbg committed 4 years ago

788ccf07

feat(data/equiv/mul_add): add to_additive attribute to `group.is_unit` (#12563)

adomani committed 4 years ago

cd111e94

chore(set_theory/ordinal_arithmetic): Make auxiliary result private (#12562)

vihdzp committed 4 years ago

41f5c176

chore(measure_theory/function/convergence_in_measure): golf proof with Borel-Cantelli (#12551)

kex-y committed 4 years ago

4048a9be

feat(set_theory/ordinal_arithmetic): `add_eq_zero_iff`, `mul_eq_zero_iff` (#12561)

vihdzp committed 4 years ago

d56a9bc2

refactor(group_theory/commutator): Generalize `map_commutator_element` (#12555)

tb65536 committed 4 years ago

1e560a67

refactor(topology/opens): Turn `opens.gi` into a Galois coinsertion (#12547)

YaelDillies committed 4 years ago

24e3b5f5

feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490)

CBirkbeck committed 4 years ago

0fd99294

chore(linear_algebra/affine_space/affine_map): golf using the injective APIs (#12543)

eric-wieser committed 4 years ago

750ca956

fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action (#12541)

eric-wieser committed 4 years ago

8836a42d

feat(field_theory/krull_topology): added krull_topology_totally_disconnected (#12398)

Sebastian-Monnet committed 4 years ago

9e288527

feat(topology/opens): The frame of opens of a topological space (#12546)

YaelDillies committed 4 years ago

bab039fb

feat(category_theory/abelian/exact): `exact g.op f.op` (#12456)

jjaassoonn committed 4 years ago

9c2f6ebe

Newer Older