leanprover-community/mathlib

Pull Requests Commits

kim-em committed 3 years ago

577e5563

chore(topology/metric_space/basic): golf an instance (#13664)

urkud committed 3 years ago

454b8848

docs(number_theory/sum_two_squares): Update docs (#13593)

vihdzp committed 3 years ago

9101c48b

docs(tactic/algebra): Module docstring (#13571)

YaelDillies committed 3 years ago

045fc443

feat(algebra/polynomial/big_operators): add a lemma, reduce assumptions, golf (#13264)

astrainfinita committed 3 years ago

54d1ddd2

refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)

urkud committed 3 years ago

0d16bb4d

chore(order/filter/small_sets): redefine, golf (#13672)

urkud committed 3 years ago

53a484e6

feat(data/quot): Decidability of `quotient.lift` and friends (#13589)

YaelDillies committed 3 years ago

42b9cdf8

refactor(linear_algebra/dimension): further generalisations to division_ring (#13657)

kim-em committed 3 years ago

63da426d

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

Older