leanprover-community/mathlib3

Pull Requests Commits

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

kim-em committed 4 years ago

21d033c5

kim-em committed 4 years ago

27eaca92

feat(group_theory/subgroup): Subgroup of subgroup is isomorphic to itself (#9204)

tb65536 committed 4 years ago

591ff3a5

feat(order/rel_classes): A total relation is trichotomous (#9181)

YaelDillies committed 4 years ago

463089da

chore(*): upgrade to Lean 3.33.0c (#9165)

urkud committed 4 years ago

23eac53f

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

Older