leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

995c1ac0

eric-wieser committed 3 years ago

bb30acbb

Merge remote-tracking branch 'origin/master' into eric-wieser/sigma_congr_right_sign

eric-wieser committed 3 years ago

607b3393

feat(set_theory/surreal/basic): Definitional characterization of `numeric` (#13653)

vihdzp committed 3 years ago

81262559

feat(algebra/hom/iterate): Iterating an action (#13659)

tb65536 committed 3 years ago

e006f38c

refactor(category_theory/monoidal): prove coherence lemmas by coherence (#13406)

kim-em committed 3 years ago

b8b8bf3e

feat(set_theory/game/pgame): Birthdays of pre-games (#13636)

vihdzp committed 3 years ago

92ca1369

chore(order/filter/basic): golf 2 proofs (#13614)

urkud committed 3 years ago

5998b497

chore(set_theory/game/pgame): Cleanup (#13612)

vihdzp committed 3 years ago

946f253c

docs(tactic/lint/default): Module docstring (#13570)

YaelDillies committed 3 years ago

b0552c15

chore(algebra/*): move function instances (#13650)

eric-wieser committed 3 years ago

2d0ff329

feat(algebra/ring/basic): generalisation linter suggestions (#13649)

ericrbg committed 3 years ago

cc406db0

chore(group_theory/exponent): generalise (#13647)

ericrbg committed 3 years ago

1abfde6c

feat(set_theory/game/pgame): Strengthen `move_{left/right}_mk` (#13646)

vihdzp committed 3 years ago

34b1cfd8

fix(topology/algebra/matrix): correct a lemma name (#13640)

eric-wieser committed 3 years ago

44a05db5

feat(data/part): add get_or_else_of_dom (#13588)

BoltonBailey committed 3 years ago

09eb35fd

feat(order/hom/basic): add simp lemmas for `strict_mono.order_iso` and friends (#13606)

ocfnash committed 3 years ago

afd8a525

chore(analysis/normed_space/ray): golf (#13629)

urkud committed 3 years ago

8c262dae

chore(algebra/ring/equiv): protect ring equiv lemmas for big operators (#13624)

j-loreaux committed 3 years ago

4ad7dc9d

feat(algebra/algebra/basic,analysis/normed_space/basic): The zero ring is a (normed) algebra (#13618)

eric-wieser committed 3 years ago

fe435de8

feat(set_theory/pgame): Lemmas about order and left/right moves (#13590)

vihdzp committed 3 years ago

0bea7a08

feat(set_theory/game/pgame): Empty instances (#13635)

vihdzp committed 3 years ago

26b2d727

feat(linear_algebra/basic): add a simp lemma for comp_right (#13625)

antoinelab01 committed 3 years ago

94f970a6

doc(analysis/normed_space/basic): Explain how to use non-unital normed algebras (#13605)

eric-wieser committed 3 years ago

b62b5314

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

leanprover-community-bot committed 3 years ago

79ea30ce

doc(measure_theory): add some missing `to_additive` docstrings (#13456)

urkud committed 3 years ago

9923362c

feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602)

YaelDillies committed 3 years ago

976c544c

feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534)

eric-wieser committed 3 years ago

b98bd418

chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)

Ruben-VandeVelde committed 3 years ago

45470769

feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308)

YaelDillies committed 3 years ago

9eb3858a

Older