leanprover-community/mathlib

Pull Requests Commits

feat(analysis/normed_space/finite_dimension): Riesz theorem on compact unit ball and finite dimension (#9147)

sgouezel committed 4 years ago

82dced60

feat(ring_theory/adjoin): adjoin_range_eq_range_aeval (#9179)

ChrisHughes24 committed 4 years ago

27b0a763

chore(combinatorics/simple_graph): fixup docs (#9161)

ericrbg committed 4 years ago

bf0b5df3

ci(.github/workflows/*): lint PR style on GitHub runners (#9198)

bryangingechen committed 4 years ago

ec118ddc

chore(order/pilex): use `*_order_of_*TO` from `order.rel_classes` (#9129)

urkud committed 4 years ago

6a6b0a56

chore(*): simplify `data.real.cau_seq` import (#9197)

Vierkantor committed 4 years ago

91f053e1

feat(group_theory/p_group): Intersection with p-subgroup is a p-subgroup (#9189)

tb65536 committed 4 years ago

e489ca1d

refactor(group_theory/p_group): Move lemmas to is_p_group namespace (#9188)

tb65536 committed 4 years ago

eb203909

chore(ring_theory/adjoin) elab_as_eliminator attribute (#9168)

ChrisHughes24 committed 4 years ago

6309c816

feat(ring_theory/nakayama): Alternative Statements of Nakayama's Lemma (#9150)

ChrisHughes24 committed 4 years ago

251e418a

feat(linear_algebra/free_module): add instances (#9072)

riccardobrasca committed 4 years ago

19949a07

feat(group_theory/free_product): equivalence with reduced words (#7395)

dwarn committed 4 years ago

2a3cd41b

chore(data/fintype/intervals): finiteness of `Ioo`, `Ioc`, and `Icc` over `ℕ` (#9096)

FrickHazard committed 4 years ago

7deb32cb

feat(measure_theory/measure/integral): integral over an encodable type (#9191)

urkud committed 4 years ago

2d57545b

feat(linear_algebra/matrix/is_diag): add a file (#9010)

l534zhan committed 4 years ago

790e98fb

feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure (#9186)

kex-y committed 4 years ago

9af1db3c

chore(order/bounded_lattice): make `bot_lt_some` and `some_lt_none` consistent (#9180)

YaelDillies committed 4 years ago

ceab0e7f

feat(measure_theory/function/lp_space): add lemmas about snorm and mem_Lp (#9146)

RemyDegenne committed 4 years ago

ef78b322

chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file (#9111)

sgouezel committed 4 years ago

5aaa5faa

feat(data/last/basic): a lemma specifying list.split_on (#9104)

kim-em committed 4 years ago

4b7593fc

feat(group_theory/p_group): Bottom subgroup is a p-group (#9190)

tb65536 committed 4 years ago

d3b345df

feat(topology): one-point compactification of a topological space (#8579)

justadzr committed 4 years ago

8dffafd2

chore(scripts): update nolints.txt (#9192)

leanprover-community-bot committed 4 years ago

f88f3a76

feat(linear_algebra/matrix/circulant): add a file (#9011)

l534zhan committed 4 years ago

f0a1356c

feat(data/(d)finsupp): (d)finsupp.update (#9015)

pechersky committed 4 years ago

103c1ffa

fix(tactic/rcases): Don't parameterize parsers (#9159)

digama0 committed 4 years ago

d9476d44

feat(README.md): add Rémy Degenne (#9187)

jcommelin committed 4 years ago

ec5f4961

feat(measure_theory/measure/vector_measure): add `vector_measure.trim` (#9169)

kex-y committed 4 years ago

40247bd5

feat(linear_algebra/determinant): more on the determinant of linear maps (#9139)

sgouezel committed 4 years ago

3b4f4daf

chore(analysis/calculus/[f]deriv): generalize product formula to product in normed algebras (#9163)

ADedecker committed 4 years ago

a9e7d333

Older