leanprover-community/mathlib3

Pull Requests Commits

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

chore(algebra/big_operators): add a lemma (#9120)

urkud committed 4 years ago

ad625833

feat(group_theory/nilpotent): add intermediate lemmas (#9016)

ineswright committed 4 years ago

b0e8ced1

feat(group_theory/p_group): Generalize to infinite p-groups (#9082)

tb65536 committed 4 years ago

a8a8edcb

feat(measure_theory/measure/with_density_vector_measure): define vector measures by an integral over a function (#9008)

kex-y committed 4 years ago

d4f8b921

feat(number_theory/padics/padic_integers): Z_p is adically complete (#8995)

jcommelin committed 4 years ago

80085fc2

feat(analysis/convex/independent): convex independence (#9018)

YaelDillies committed 4 years ago

d0820017

chore(order/filter): more readable proof (#9173)

PatrickMassot committed 4 years ago

1cf17041

chore(ring_theory/polynomial/cyclotomic): fix namespacing (#9116)

ericrbg committed 4 years ago

14790682

feat(linear_algebra/adic_completion): le_jacobson_bot (#9125)

adamtopaz committed 4 years ago

56511573

feat(set_theory/surreal): add dyadic surreals (#7843)

apurvnakade committed 4 years ago

ca23d52c

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

leanprover-community-bot committed 4 years ago

f0effbda

feat(group_theory/perm/concrete_cycle): perms from cycle data structure (#8866)

pechersky committed 4 years ago

87c1820c

feat(order/zorn) : `chain_univ` (#9162)

YaelDillies committed 4 years ago

f6c8affd

chore(linear_algebra/basic): move map_comap_eq into submodule namespace (#9160)

ChrisHughes24 committed 4 years ago

5b702ec3

doc(algebra/covariant_and_contravariant): fix parameter documentation… (#9171)

itaibn committed 4 years ago

00d570af

chore(algebra/field_power): golf some proofs (#9170)

Ruben-VandeVelde committed 4 years ago

65f8148b

feat(data/fin): eq_zero_or_eq_succ (#9136)

kim-em committed 4 years ago

3366a685

chore(category/abelian/pseudoelements): localize expensive typeclass (#9156)

kim-em committed 4 years ago

a7d872fa

feat(logic/basic): a few lemmas (#9166)

urkud committed 4 years ago

995f4819

feat(ring_theory/ideal/operations): annihilator_smul (#9151)

ChrisHughes24 committed 4 years ago

04d2b12e

fix(category_theory/concrete_category): remove bad instance (#9154)

kim-em committed 4 years ago

f8637039

fix(ring_theory/ideal/basic): ideal.module_pi speedup (#9148)

kbuzzard committed 4 years ago

858e7649

feat(category_theory/monoidal): rigid (autonomous) monoidal categories (#8946)

javra committed 4 years ago

b55483ae

fix(category_theory/adjunction/limits): remove bad instance (#9157)

kim-em committed 4 years ago

e1bed5a0

fix(category/preadditive/single_obj): remove superfluous instance (#9155)

kim-em committed 4 years ago

059eba46

Newer Older