leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 4 years ago

441a1d89

Merge branch 'eric-wieser/dedup-direct_sum.ring_hom_ext' into eric-wieser/unbundle-direct_sum.of

eric-wieser committed 4 years ago

d6d35c4d

fix(algebra/direct_sum): change `ring_hom_ext` to not duplicate `ring_hom_ext'`

eric-wieser committed 4 years ago

fe9968b0

refactor(algebra/direct_sum): unbundle `direct_sum.of`

eric-wieser committed 4 years ago

9538e774

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

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

digama0 committed 4 years ago

a7b4018a

feat(algebraic_geometry): Explicit description of the colimit of presheafed spaces. (#10466)

erdOne committed 4 years ago

df931664

feat(algebraic_geometry): Open immersions of presheafed spaces (#10437)

erdOne committed 4 years ago

b7ed03f9

feat(algebra/monoid_algebra/grading): internal graded structure for an arbitrary degree function (#10435)

yuma-mizuno committed 4 years ago

2f44ac8f

feat(category_theory/*): Representably flat functors (#9519)

erdOne committed 4 years ago

f0a1cd1a

Older