leanprover-community/mathlib3

Pull Requests Commits

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

adomani committed 3 years ago

9ecd5e66

Merge branch 'master' into adomani_move_add_random_golf

adomani committed 3 years ago

8255b218

feat(*/sub*/pointwise): lemmas about pointwise scalar actions (#17814)

eric-wieser committed 3 years ago

c982179e

chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811)

adomani committed 3 years ago

ce613251

feat(algebra/order/zero_le_one): generalize lemmas (#17465)

astrainfinita committed 3 years ago

9b2660e1

feat(group_theory): generalize `normal_map` (#17808)

urkud committed 3 years ago

cc3c8aa5

feat(linear_algebra/affine_space/finite_dimensional): more affine independence / collinearity lemmas (#17643)

jsm28 committed 3 years ago

6c5959aa

feat(data/real/basic): remove typeclass shortcircuit (#17804)

hrmacbeth committed 3 years ago

1a766f5a

feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023)

kim-em committed 3 years ago

4ed0bcae

adomani committed 3 years ago

28dedc38

feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492)

kkytola committed 3 years ago

6b766f92

adomani committed 3 years ago

c785e131

Merge branch 'master' into adomani_move_add_random_golf

adomani committed 3 years ago

ac95b7c2

feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801)

YaelDillies committed 3 years ago

dad7ecf9

chore(algebra/group/conj): move out results about finiteness (#17789)

Ruben-VandeVelde committed 3 years ago

d4ebdc81

fix(scripts/port_comments): deal with files that have no header to insert below (#17797)

eric-wieser committed 3 years ago

32e4a38c

chore(nat/order/basic): remove implicit variables (#17707)

Multramate committed 3 years ago

acf5258c

feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)

joelriou committed 3 years ago

31019c25

feat(algebra/order/group/defs): add choice-free shortcut instances for `ordered_comm_group` (#17564)

astrainfinita committed 3 years ago

011aebd9

doc(tactic/congr): add relationship to `move_add` in `ac_change` (#14618)

adomani committed 3 years ago

28b66e1a

feat(topology/algebra/module/finite_dimension): `can_lift` instances (#17773)

YaelDillies committed 3 years ago

246853d5

feat(quiver/basic): push arrows of a quiver along a map (#17618)

bottine committed 3 years ago

7ba713a7

chore(algebra/star/basic): split out `big_operators` import (#17792)

hrmacbeth committed 3 years ago

6f6739f8

chore(data/set/pointwise/basic): split (#17768)

hrmacbeth committed 3 years ago

9114ddff

feat({data/finset/basic, ring_theory/roots_of_unity, algebra/ring/units}): add lemmas (#17671)

riccardobrasca committed 3 years ago

084ba5e0

chore(measure_theory/measurable_space_def): delete unused import (#17799)

hrmacbeth committed 3 years ago

94c141ac

feat(data/polynomial/basic): add to_finsupp_C_mul_X_pow lemmas (#17794)

Multramate committed 3 years ago

e574b1a4

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

leanprover-community-bot committed 3 years ago

308f6d03

chore(data/real/cau_seq): generalize to noncommutative settings (#17785)

eric-wieser committed 3 years ago

e469260a

feat(algebra/group/pi): add pi.monoid_hom (#17757)

xroblot committed 3 years ago

76658a41

Older