leanprover-community/mathlib

Pull Requests Commits

ci(*): tweak synchronization bot behavior (#17693)

eric-wieser committed 3 years ago

9407a363

chore(linear_algebra/matrix/sesquilinear_form): fix a timeout (#17705)

riccardobrasca committed 3 years ago

bb0ad86c

feat(algebra/cubic_discriminant): add eq_zero and ne_zero lemmas (#17627)

Multramate committed 3 years ago

c1d80c11

feat(logic/function/basic): refine extend_apply (#16944)

AntoineChambert-Loir committed 3 years ago

5fce1791

lint(*/finsupp/*): use `finite` instead of `fintype` (#17553)

urkud committed 3 years ago

5fd3186f

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

leanprover-community-bot committed 3 years ago

6b3325cd

chore(data/list/big_operators): split (#17702)

hrmacbeth committed 3 years ago

364d8714

chore(data/fin/basic): downgrade `data.nat.order` import (#17691)

hrmacbeth committed 3 years ago

eb620d2d

doc(data/nat/prime): `prime` ≠ `nat.prime` (#17689)

ericrbg committed 3 years ago

f340f229

docs(tactic/move_add): fix doc-strings and links (#17684)

adomani committed 3 years ago

205a628e

feat(data/polynomial/ring_division): add `roots_pow`, `roots_monomial` (#17663)

urkud committed 3 years ago

c78ee2be

feat(scripts/port_status): output `git diff` command (#17630)

ericrbg committed 3 years ago

1507ed4a

chore(docs/undergrad): mention continuity and differentiability of series of functions (#17682)

sgouezel committed 3 years ago

5e58a9dd

feat(probability/probability_mass_function/*): Define `pmf` in terms of `ennreal` instead of `nnreal` (#17032)

dtumad committed 3 years ago

e50b8c26

feat(geometry/euclidean/angle/oriented/basic): rotation and negation lemmas (#17277)

jsm28 committed 3 years ago

286e6bab

feat(linear_algebra/affine_space/affine_map): `line_map_eq_` `iff` lemmas (#17658)

jsm28 committed 3 years ago

79f700b0

fix(topology/fiber_bundle/basic): make argument of fiber_bundle_core.to_topological_space implicit (#17678)

fpvandoorn committed 3 years ago

f11f1e72

feat(geometry/euclidean/angle/oriented/affine): `π / 2` lemmas (#17487)

jsm28 committed 3 years ago

1534854c

feat(geometry/euclidean/angle/sphere): affine circle theorems (#17279)

jsm28 committed 3 years ago

8d9836ff

feat(geometry/euclidean/angle/oriented): nonzero angle lemmas (#17272)

jsm28 committed 3 years ago

da5e1327

fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679)

fpvandoorn committed 3 years ago

8bab60f0

chore(geometry/manifold/mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675)

CBirkbeck committed 3 years ago

98cdae56

feat(ring_theory/ideal): ideal norm evaluation lemmas (#17299)

Vierkantor committed 3 years ago

31c458dc

feat(analysis/calculus): smoothness of series of functions (#17110)

sgouezel committed 3 years ago

563bbc0c

feat(analysis/normed/group/add_circle): results about finite-order points on the circle (#17321)

ocfnash committed 3 years ago

084f76e2

chore(linear_algebra/linear_pmap): leq lemma (#17565)

mcdoll committed 3 years ago

8709a597

feat(data/finite/defs): add `ulift.infinite`/`plift.infinite` (#17655)

urkud committed 3 years ago

f69e8f31

feat(data/list/big_operators): add lemmas on products/sums (#17499)

MichaelStollBayreuth committed 3 years ago

cadea043

perf(analysis/complex/conformal): squeeze simps (#17667)

j-loreaux committed 3 years ago

3403c032

feat(order/modular_lattice): Modular lattices are lower modular (#17403)

MadPidgeon committed 3 years ago

124aa163

Newer Older