leanprover-community/mathlib3

Pull Requests Commits

a couple more tweaks

jcommelin committed 4 years ago

d27189e3

jcommelin committed 4 years ago

647cdcc5

jcommelin committed 4 years ago

4d7e081a

jcommelin committed 4 years ago

70b958df

Merge branch 'master' into imo2001_q6

jcommelin committed 4 years ago

f4612635

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

RemyDegenne committed 4 years ago

9e320a22

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

urkud committed 4 years ago

ea772710

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

YaelDillies committed 4 years ago

3788cbfa

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

ocfnash committed 4 years ago

87e9becc

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

jcommelin committed 4 years ago

0a79eec3

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

YaelDillies committed 4 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 4 years ago

d7579961

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

justadzr committed 4 years ago

b3c1de6a

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

eric-wieser committed 4 years ago

2f29e090

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

urkud committed 4 years ago

1b876c7d

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

pechersky committed 4 years ago

88f9480d

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

sgouezel committed 4 years ago

a23c47ca

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

adomani committed 4 years ago

da32780c

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

pechersky committed 4 years ago

b9e4c084

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

sgouezel committed 4 years ago

59c8befc

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

urkud committed 4 years ago

f471b899

feat(order/bounded_lattice): define the `distrib_lattice_bot` typeclass (#8507)

YaelDillies committed 4 years ago

dc6adcc8

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

leanprover-community-bot committed 4 years ago

e28d9451

feat(logic/unique,data/fintype/basic): unique and fintype of subtype of one element (#8491)

pechersky committed 4 years ago

c2a0532f

docs(order/complete_boolean_algebra): add module docstring, add whitespaces (#8525)

YaelDillies committed 4 years ago

eb73c357

feat(logic/basic): `ite p a b` is equal to `a` or `b` (#8557)

YaelDillies committed 4 years ago

c2ed7dcc

refactor(order/disjointed): generalize `disjointed` to generalized boolean algebras (#8409)

YaelDillies committed 4 years ago

52b6516b

feat(data/matrix/basic): add `alg_(hom|equiv).map_matrix` (#8527)

eric-wieser committed 4 years ago

8e79ea53

feat(linear_algebra/clifford_algebra): the reals and complex numbers have isomorphic real clifford algebras (#8165)

eric-wieser committed 4 years ago

a0cb45fe

chore(category_theory/whiskering): Fix docstring (#8533)

adamtopaz committed 4 years ago

ee8e447e

Older