leanprover-community/mathlib

Pull Requests Commits

feat(algebra/order_functions): lt_max_of_lt_<left/right> (#7849)

YaelDillies committed 4 years ago

4bfe8e8a

feat(topology/algebra/ordered/basic): add a few subseq-related lemmas (#7828)

ADedecker committed 4 years ago

915a0a21

chore(algebra/lie/classical): speed up slow proof (#7894)

sgouezel committed 4 years ago

51cd821b

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

leanprover-community-bot committed 4 years ago

6eb3d971

feat(set_theory/cardinal): missing lemma (#7880)

kim-em committed 4 years ago

6f6dbad6

doc(int/modeq): add module doc and tidy (#7878)

ericrbg committed 4 years ago

e8aa9849

chore(data/real/nnreal): avoid abusing inequalities in nnreals (#7872)

adomani committed 4 years ago

1b0e5ee5

feat(logic/function/basic): a lemma on symmetric operations and flip (#7871)

adomani committed 4 years ago

d5705960

chore(data/real/pi, analysis/special_functions/trigonometric.lean): speed up/simplify proofs (#7868)

adomani committed 4 years ago

9a4881d4

chore(logic/basic): fixup `eq_or_ne` (#7865)

ericrbg committed 4 years ago

f157a372

chore(analysis/normed_space/normed_group_hom): remove bound_by (#7860)

riccardobrasca committed 4 years ago

0a80efb3

feat(algebra/big_operators/finsupp): relax assumptions `semiring` to `non_unital_non_assoc_semiring` (#7874)

ocfnash committed 4 years ago

0f8e79ea

chore(src/testing/slim_check/sampleable): simply add explicit namespace `nat.` (#7873)

adomani committed 4 years ago

3b5a44b8

feat(algebra/floor): nat_floor (#7855)

YaelDillies committed 4 years ago

2e8ef55f

feat(analysis/special_functions/pow): rpow-log inequalities (#7848)

YaelDillies committed 4 years ago

021c8590

feat(algebra/ordered_ring): more granular typeclasses for `with_top α` and `with_bot α` (#7845)

eric-wieser committed 4 years ago

49f5a159

Revert "feat(set_theory/cofinality): more infinite pigeonhole principles"

kim-em committed 4 years ago

079b8a11

feat(set_theory/cofinality): more infinite pigeonhole principles

kim-em committed 4 years ago

c7ba50f4

chore(algebra/linear_ordered_comm_group_with_zero.lean): extend calc proofs (#7870)

adomani committed 4 years ago

f7e93d9e

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

leanprover-community-bot committed 4 years ago

05b7b0b0

chore(number_theory/{fermat4, sum_four_squares, zsqrtd/basic}): simplify/rearrange proofs (#7866)

adomani committed 4 years ago

4da899c0

feat(algebra/group_with_zero): add units.can_lift (#7857)

eric-wieser committed 4 years ago

2fc66c92

chore(topology/algebra/continuous_functions): making names consistent with the smooth library (#7844)

Nicknamen committed 4 years ago

0a348784

feat(ring_theory/ideal): generalize to noncommutative rings (#7654)

kim-em committed 4 years ago

06200c84

doc(data/semiquot): reformat module doc properly, and add missing doc strings (#7773)

kim-em committed 4 years ago

3870896a

docs(data/mllist): fix module doc, and add all doc strings (#7772)

kim-em committed 4 years ago

abe25e96

feat(measure_theory/tactic): add measurability tactic (#7756)

RemyDegenne committed 4 years ago

d9b91f3b

chore(geometry/euclidean/circumcenter): remove two `have`s in a proof (#7852)

adomani committed 4 years ago

8e25717f

chore(measure_theory/set_integral): put the definition of integrable_on into a new file (#7842)

RemyDegenne committed 4 years ago

d0ed2a42

feat(algebra/ordered_group): `-abs a ≤ a` (#7839)

benjamindavidson committed 4 years ago

764e878e

Newer Older