leanprover-community/mathlib3

Pull Requests Commits

jjaassoonn committed 4 years ago

201e5ac2

It should be ok now

jjaassoonn committed 4 years ago

9bd35a37

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

jjaassoonn committed 4 years ago

9251cacb

awaiting for CI

jjaassoonn committed 4 years ago

27c9237f

Merge branch 'graded_ring_dep_4' into graded_ring_dep_6

jjaassoonn committed 4 years ago

b348a312

jjaassoonn committed 4 years ago

cd8993ba

jjaassoonn committed 4 years ago

95ee79e3

Update src/ring_theory/graded_algebra/basic.lean

jjaassoonn committed 4 years ago

Verified fdfd8297

Merge remote-tracking branch 'origin/master' into graded_ring_dep_4

jjaassoonn committed 4 years ago

277689b3

jjaassoonn committed 4 years ago

04326043

Update src/algebra/graded_monoid.lean

jjaassoonn committed 4 years ago

Verified b66840c2

Update src/algebra/graded_monoid.lean

jjaassoonn committed 4 years ago

Verified c0bb693e

Update src/algebra/graded_monoid.lean

jjaassoonn committed 4 years ago

Verified 2dab0d07

apply suggestions from @eric-wieser

jjaassoonn committed 4 years ago

567f2a89

feat(data/finsupp/basic): lemmas on the support of the `tsub` of `finsupp`s (#10651)

stuart-presnell committed 4 years ago

08215b55

feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590)

RemyDegenne committed 4 years ago

9ef122d2

feat(group_theory/submonoid): The monoid_hom from a submonoid to its image. (#10680)

erdOne committed 4 years ago

c23b54c7

feat(analysis/calculus/deriv): generalize some lemmas (#10639)

urkud committed 4 years ago

97e44687

feat(order/filter,topology/instances/real): lemmas about `at_top`, `at_bot`, and `cocompact` (#10652)

urkud committed 4 years ago

bfe595d3

chore(measure_theory/function/conditional_expectation): change condexp notation (#10584)

RemyDegenne committed 4 years ago

e3d9adf1

feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490)

urkud committed 4 years ago

70171ac4

chore(algebra/direct_limit): remove module.directed_system (#10636)

eric-wieser committed 4 years ago

4efa9d8a

feat(analysis/normed_space/weak_dual): add polar sets in preparation for Banach-Alaoglu theorem (#9836)

kkytola committed 4 years ago

11bf7e52

doc(data/nat/prime): fix links (#10677)

ericrbg committed 4 years ago

fc3116f9

feat(data/finset/basic): val_le_iff_val_subset (#10603)

isadofschi committed 4 years ago

ab316732

feat(data/mv_polynomial/basic) induction_on'' (#10621)

isadofschi committed 4 years ago

60c1d60e

feat(data/int/basic): add `nat_abs_eq_nat_abs_iff_*` lemmas for nonnegative and nonpositive arguments (#10611)

stuart-presnell committed 4 years ago

e14dc11a

refactor(data/matrix): reverse the direction of `matrix.minor_mul_equiv` (#10657)

Vierkantor committed 4 years ago

baab5d30

feat(data/list/range): fin_range_succ_eq_map (#10654)

eric-wieser committed 4 years ago

2ea1fb68

chore(algebra/tropical/basic): golf and clean (#10633)

pechersky committed 4 years ago

fdb773a2

Older