leanprover-community/mathlib

Pull Requests Commits

jjaassoonn committed 4 years ago

4b88db2f

remove group_theory change

jjaassoonn committed 4 years ago

5f95dfc5

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

jjaassoonn committed 4 years ago

36b46cf7

homogeneous_element

jjaassoonn committed 4 years ago

7465b147

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

I need to wait for this be cached, otherwise nothign compiles

jjaassoonn committed 4 years ago

94a38bf1

Merge branch 'graded_ring_dep_3' into graded_ring_dep_4

jjaassoonn committed 4 years ago

9e7e72a8

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

jjaassoonn committed 4 years ago

3a74f9e8

Merge branch 'master' into graded_ring_dep_4

jjaassoonn committed 4 years ago

43d5acfa

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

mans0954 committed 4 years ago

428b9e55

moved things around

jjaassoonn committed 4 years ago

c80995df

Update basic.lean

jjaassoonn committed 4 years ago

Verified 84579b2d

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

this should fix it

jjaassoonn committed 4 years ago

692ae2e8

jjaassoonn committed 4 years ago

3fb5d8d5

remove unnecessary lemma

jjaassoonn committed 4 years ago

fece57e0

added missing lemma

jjaassoonn committed 4 years ago

6094f3cd

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

Ruben-VandeVelde committed 4 years ago

cd2230b4

Newer Older