leanprover-community/mathlib3

Pull Requests Commits

feat(ring_theory/noetherian): add noeth ring lemma (#8566)

kbuzzard committed 5 years ago

8edcf906

feat(algebra/ordered_field): add `inv_le_of_inv_le` and `inv_lt_of_inv_lt` (#8565)

urkud committed 5 years ago

5f2d9548

feat(matrix/kronecker): Add the Kronecker product (#8560)

eric-wieser committed 5 years ago

f29cc59f

fix(analysis/normed_space/basic): add an alias instance to fix an inference issue (#8547)

eric-wieser committed 5 years ago

7b1ce10b

chore(data/pfun): rename `roption` to `part`, split `data.part` off `data.pfun` (#8544)

YaelDillies committed 5 years ago

fb63cf3e

chore(data/finsupp): add missing lemmas (#8553)

eric-wieser committed 5 years ago

67282017

chore(galois_connection): golf some proofs (#8582)

urkud committed 5 years ago

3f5a348f

feat(group_theory/sylow): Generalize proof of first Sylow theorem (#8383)

ChrisHughes24 committed 5 years ago

24bbbdce

feat(category_theory/adjunction): general adjoint functor theorem (#4885)

b-mehta committed 5 years ago

4813b73a

feat(group_theory/group_action): Cayley's theorem (#8552)

eric-wieser committed 5 years ago

7bb4b273

chore(measure_theory/special_functions): add measurability attributes (#8570)

RemyDegenne committed 5 years ago

9e320a22

chore(analysis/calculus/{f,}deriv): fix, add missing lemmas (#8574)

urkud committed 5 years ago

ea772710

urkud committed 5 years ago

74196e2b

chore(algebra/*, data/polynomial/*): remove unnecessary imports (#8578)

YaelDillies committed 5 years ago

3788cbfa

chore(linear_algebra/matrix/trace): relax `comm_ring` to `comm_semiring` in `matrix.trace_mul_comm` (#8577)

ocfnash committed 5 years ago

87e9becc

urkud committed 5 years ago

46a5a106

fix(order/bounds): remove double space (#8575)

jcommelin committed 5 years ago

0a79eec3

refactor(data/nat/choose): reduce assumptions on lemmas (#8508)

YaelDillies committed 5 years ago

575fcc65

feat(analysis/complex): prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential (#8424)

justadzr committed 5 years ago

d7579961

Merge branch 'inv-le-of-inv-le' into ccl-Sup

urkud committed 5 years ago

5b20d49d

Merge branch 'master' into ccl-Sup

urkud committed 5 years ago

7720934f

feat(analysis/complex/basic): add several trivial lemmas for differentiable functions. (#8418)

justadzr committed 5 years ago

b3c1de6a

feat(group_action/defs): generalize faithful actions (#8555)

eric-wieser committed 5 years ago

2f29e090

chore(algebra/ordered_group): fix/add `order_dual` instances, add lemmas (#8564)

urkud committed 5 years ago

1b876c7d

feat(logic/embedding): subtype_or_{embedding,equiv} (#8489)

pechersky committed 5 years ago

88f9480d

feat(topology/instances/ennreal): ediam of intervals (#8546)

sgouezel committed 5 years ago

a23c47ca

chore(data/polynomial/*): create file `data/polynomial/inductions` and move around lemmas (#8563)

adomani committed 5 years ago

da32780c

refactor(algebra/regular): split out `is_regular` (#8561)

pechersky committed 5 years ago

b9e4c084

feat (order/liminf_limsup): frequently_lt_of_lt_limsup (#8548)

sgouezel committed 5 years ago

59c8befc

feat(topology,geometry/manifold): continuous and smooth partition of unity (#8281)

urkud committed 5 years ago

f471b899

Newer Older