leanprover-community/mathlib3

Pull Requests Commits

feat(data/set/Union_lift): lift functions to Unions of sets (#9019)

ChrisHughes24 committed 4 years ago

b63c5601

chore(ring_theory/ideal/operations): golf a definition using new actions (#9152)

eric-wieser committed 4 years ago

25972642

chore(data/dfinsupp): golf using `quotient.map` instead of `quotient.lift_on` (#9176)

eric-wieser committed 4 years ago

3a6340cc

refactor(logic/relator): turn *_unique and *_total into defs, not classes (#9135)

urkud committed 4 years ago

f8d8171d

feat(category_theory/filtered): Special support for bowtie and tulip diagrams (#9099)

justus-springer committed 4 years ago

f1bf7b87

feat(ring_theory/artinian): is_nilpotent_jacobson (#9153)

ChrisHughes24 committed 4 years ago

bb38ce96

refactor(measure_theory/measure): redefine `measure_theory.sigma_finite` (#9207)

urkud committed 4 years ago

85dc9f34

refactor(measure_theory/integral/lebesgue): golf a proof (#9206)

urkud committed 4 years ago

7492aa60

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

Newer Older