leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 3 years ago

41cf0cc2

chore(*): add mathlib4 synchronization comments (#17686)

leanprover-community-bot committed 3 years ago

cb1d2791

docs(src/algebra/group/unique_prods): replace `*` with `+` in a `to_additive` doc-string (#17710)

adomani committed 3 years ago

71ca4770

feat(data/quot,data/set/basic): add lemmas about `lift` (#17699)

urkud committed 3 years ago

84582d28

feat(group_theory/subgroup/basic): weaken some TC assumptions (#17698)

urkud committed 3 years ago

208d8866

feat(geometry/euclidean/angle/oriented/basic): `π / 2` rotations and inner product (#17687)

jsm28 committed 3 years ago

fe3cd450

feat(measure_theory/integral): change of variables for integrals over `Ioi` domains (#17542)

loefflerd committed 3 years ago

e45547e5

feat(measure_theory/group/fundamental_domain): add lemma `measure_theory.is_fundamental_domain.mk_of_measure_univ_le` (#17438)

ocfnash committed 3 years ago

e4edb230

feat(topology/metric_space/hausdorff_distance): Add lemmas about frontiers of thickenings. (#17358)

kkytola committed 3 years ago

c7841093

feat(logic.basic): add ne_and_eq_iff_right (#17673)

riccardobrasca committed 3 years ago

2397ca3a

feat (analysis/fourier): Fourier analysis on the additive circle (#17598)

loefflerd committed 3 years ago

7922df8f

feat(algebra/group/defs): add is_cancel_mul (#17440)

riccardobrasca committed 3 years ago

497384a6

refactor(data/polynomial/ring_division): Generalize `irreducible_of_monic` to `no_zero_divisors` (#17696)

tb65536 committed 3 years ago

86754809

refactor(order/conditionally_complete_lattice): split file (#17695)

kim-em committed 3 years ago

1d94b2ea

refactor(data/list/sublists): move lemmas to remove as import (#17694)

kim-em committed 3 years ago

3fcc5a49

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

Newer Older