leanprover-community/mathlib

Pull Requests Commits

jcommelin committed 4 years ago

110c4089

feat(linear_algebra/multilinear/basic,linear_algebra/alternating): comp_linear_map lemmas (#10631)

jsm28 committed 4 years ago

f103ae72

chore(linear_algebra/affine_space/basis): remove unhelpful coercion (#10637)

ocfnash committed 4 years ago

1ad1be71

chore(analysis/inner_product/projections): generalize some lemmas (#10608)

urkud committed 4 years ago

8438172d

refactor(order/atoms): is_simple_order from is_simple_lattice (#10537)

pechersky committed 4 years ago

e81d2ca8

chore(scripts/mk_all.sh): allow 'mk_all.sh ../test' (#10628)

kim-em committed 4 years ago

ae5e7cd4

chore(combinatorics/simple_graph/coloring): remove extra asterisk (#10618)

kmill committed 4 years ago

4ce0899b

feat(ring_theory/graded_algebra): projection map of graded algebra (#10116)

jjaassoonn committed 4 years ago

cb2777cb

feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322)

mans0954 committed 4 years ago

0a28adf1

chore(data/stream): merge `basic` into `init` (#10617)

urkud committed 4 years ago

26353ec1

fix(topology/algebra/uniform_field): remove unnecessary topological_r… (#10614)

kbuzzard committed 4 years ago

25a5c45a

chore(topology/continuous_function): remove forget_boundedness (#10612)

RemyDegenne committed 4 years ago

f0a6c99b

chore(algebra/module): generalize `char_zero.of_algebra` to `char_zero.of_module` (#10609)

urkud committed 4 years ago

2a59dffe

chore(order/galois_connection): upgrade `is_glb_l` to `is_least_l` (#10606)

urkud committed 4 years ago

2b397990

chore(order/complete_lattice): golf a proof (#10607)

urkud committed 4 years ago

d425e693

feat(number_theory/modular): the action of `SL(2, ℤ)` on the upper half plane (#8611)

AlexKontorovich committed 4 years ago

727d2372

feat(combinatorics/simple_graph): Graph coloring and partitions (#10287)

arthurpaulino committed 4 years ago

99d5c09c

chore(measure_theory/function/conditional_expectation): golf condexp_L1 proofs using set_to_fun lemmas (#10592)

RemyDegenne committed 4 years ago

d69ec4d7

feat(*): `A ⧸ B` notation for quotients in algebra (#10501)

Vierkantor committed 4 years ago

644dae26

feat(group_theory/order_of_element): order of a product of elements (#10399)

Julian-Kuelshammer committed 4 years ago

b5b26fde

feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_two_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas (#10514)

mans0954 committed 4 years ago

98cd9e42

chore(data/nat/prime): golf some proofs (#10599)

Ruben-VandeVelde committed 4 years ago

2c99a4c6

fix(tactic/abel): handle smul on groups (#10587)

digama0 committed 4 years ago

b5a26ca7

feat(probability_theory/stopping): generalize a lemma (#10598)

kex-y committed 4 years ago

a6f55313

feat(data/finset/lattice): add sup_eq_bot_iff and inf_eq_top_iff (#10596)

alexjbest committed 4 years ago

113b2658

feat(data/(mv_)polynomial): add aeval_prod and aeval_sum for (mv_)polynomial (#10594)

alexjbest committed 4 years ago

1803a678

feat(category_theory/limits): Strict terminal objects. (#10582)

erdOne committed 4 years ago

ac991c9a

feat(topology/sheaves): The empty component of a sheaf is terminal (#10578)

erdOne committed 4 years ago

1aa55c2c

chore(algebra/lattice_ordered_group): review (names, spaces, golf...) (#10595)

RemyDegenne committed 4 years ago

75cfbb3c

fix(tactic/ring): bugfixes in ring_nf (#10572)

digama0 committed 4 years ago

bf7cb6d4

Older