leanprover-community/mathlib3

Pull Requests Commits

Update basic.lean

eric-wieser committed 4 years ago

Verified 9a1ed122

feat(data/set_like/basic): add a congr lemma

eric-wieser committed 4 years ago

Verified 2b0f9691

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

jsm28 committed 4 years ago

81243140

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

ocfnash committed 4 years ago

f50984d8

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

urkud committed 4 years ago

e6ad0f29

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

pechersky committed 4 years ago

e726945e

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

kim-em committed 4 years ago

e7bd49f2

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

kmill committed 4 years ago

2b2d1167

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

jjaassoonn committed 4 years ago

8c1f2b5d

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

mans0954 committed 4 years ago

428b9e55

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

urkud committed 4 years ago

37f343cf

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

kbuzzard committed 4 years ago

6eeb54e6

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

RemyDegenne committed 4 years ago

c940e474

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

urkud committed 4 years ago

b3b7fe67

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

urkud committed 4 years ago

5d0e65aa

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

urkud committed 4 years ago

3479b7f1

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

AlexKontorovich committed 4 years ago

9c4e41ae

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

arthurpaulino committed 4 years ago

2da25ede

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

RemyDegenne committed 4 years ago

ef3540a9

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

Vierkantor committed 4 years ago

23dfe700

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

Julian-Kuelshammer committed 4 years ago

0bd9b6a3

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

1376f53d

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

Ruben-VandeVelde committed 4 years ago

cd2230b4

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

digama0 committed 4 years ago

bddc16a5

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

kex-y committed 4 years ago

46e9a235

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

alexjbest committed 4 years ago

1e897458

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

alexjbest committed 4 years ago

92fafba2

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

erdOne committed 4 years ago

4de07731

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

erdOne committed 4 years ago

d45708fc

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

RemyDegenne committed 4 years ago

1e18e93d

Older