leanprover-community/mathlib

Pull Requests Commits

feat(topology/algebra/ordered/basic): Add alternative formulations of four lemmas. (#10630)

kkytola committed 4 years ago

ba1cbfac

chore(*): fix last line length and notation style linter errors (#10642)

robertylewis committed 4 years ago

90319890

feat(data/int/basic): four lemmas about integer divisibility (#10602)

stuart-presnell committed 4 years ago

cd857f77

feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567)

ericrbg committed 4 years ago

eec4b70c

feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635)

jsm28 committed 4 years ago

a8c086fe

feat(data/multiset): add some lemmas about filter (eq x) (#10626)

Ruben-VandeVelde committed 4 years ago

1d5202ae

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

Older