leanprover-community/mathlib3

Pull Requests Commits

feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure. (#17588)

kkytola committed 3 years ago

3891ab62

feat(algebra/module/composition_series): Jordan-Hölder for modules (#17295)

MadPidgeon committed 3 years ago

cce7f68a

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

leanprover-community-bot committed 3 years ago

1fc36cc9

chore(order/bounded_order): split (#17730)

kbuzzard committed 3 years ago

97be0de9

chore(scripts/port_status.py): don't list default.lean (#17725)

kim-em committed 3 years ago

853d148d

chore(*): rename default to basic (#17724)

kim-em committed 3 years ago

829895f1

feat(data/finsupp/defs): add map_range_neg and map_range_sub (#17717)

Multramate committed 3 years ago

0f601d09

chore(topology/instances/add_circle): weaken typeclass requirements (#17729)

eric-wieser committed 3 years ago

d6aae1bc

Formatting fixes

tjeremie committed 3 years ago

c82dc978

Finished edits for first round of comments

tjeremie committed 3 years ago

19830652

Merge branch 'graphs_num_comps' of https://github.com/leanprover-community/mathlib into graphs_num_comps

tjeremie committed 3 years ago

cdf4085b

tjeremie committed 3 years ago

d2a1e993

Update src/combinatorics/simple_graph/connectivity.lean

tjeremie committed 3 years ago

Verified 3c6ca2e9

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure (#16930)

Multramate committed 3 years ago

052f6013

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

leanprover-community-bot committed 3 years ago

76171581

feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610)

kkytola committed 3 years ago

0f74a7a1

chore(algebra/support): golf, use `to_additive` (#17711)

urkud committed 3 years ago

44e2d1e4

refactor(topology/algebra/group): split file (#17697)

kim-em committed 3 years ago

717c0732

chore(analysis/complex/upper_half_plane/functions_bounded_at_infty): name updates to some lemmas (#17676)

CBirkbeck committed 3 years ago

ea579d2e

refactor(group_theory/transfer): Golf proof of `ker_transfer_sylow_disjoint` (#17661)

tb65536 committed 3 years ago

56489b55

feat(special_functions/gaussian): compute Gamma(1/2) (#17543)

loefflerd committed 3 years ago

f17ed406

feat(geometry/euclidean/angle/unoriented/affine): angles are translation invariant (#17714)

eric-wieser committed 3 years ago

01ef0f95

feat(algebra/order/monoid/with_top): add `with_top/bot.coe_pos` (#17651)

urkud committed 3 years ago

3026899c

feat(data/nat/with_bot): add nat.with_bot.add_eq_iff lemmas (#17629)

Multramate committed 3 years ago

f717251d

refactor(analysis/calculus/cont_diff): bit of cleanup (#17585)

fpvandoorn committed 3 years ago

e85b152a

feat(order/filter/lift): add `lift_map_le`, `lift'_map_le` (#17488)

urkud committed 3 years ago

443fb4e6

chore(algebra/big_operators/multiset): split (#17712)

hrmacbeth committed 3 years ago

2c459900

chore(*): rename C_mul_X to C_mul_X_pow for polynomials (#17706)

Multramate committed 3 years ago

63417e01

feat(group_theory/submonoid): add `submonoid.powers_one` (#17692)

urkud committed 3 years ago

4b4e76ca

feat(number_theory/modular_forms/slash_invariant_forms): define slash-invariant forms (#17677)

CBirkbeck committed 3 years ago

4e634b97

Newer Older