leanprover-community/mathlib3

Pull Requests Commits

switch to pathlib

BoltonBailey committed 4 years ago

ce7a2106

BoltonBailey committed 4 years ago

dad94a43

chore(data/real/pi/*): correct authorship data (#9314)

hrmacbeth committed 4 years ago

d238087f

chore(measure_theory/measurable_space): add simps config for `measurable_equiv` (#9315)

urkud committed 4 years ago

a15ae9c5

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

leanprover-community-bot committed 4 years ago

b563e5aa

refactor(group_theory/subgroup,linear_algebra/basic): put pointwise actions in their own files to match submonoid (#9312)

eric-wieser committed 4 years ago

671b1797

feat(linear_algebra/charpoly): add linear_map.charpoly (#9279)

riccardobrasca committed 4 years ago

20981bee

chore(data/equiv): rename `bool_to_equiv_prod` to `bool_arrow_equiv_prod` (#9333)

urkud committed 4 years ago

5b3b71a0

chore(ring_theory/dedekind_domain): speed up `dedekind_domain.lean` (#9232)

Vierkantor committed 4 years ago

6eb8d414

feat(algebra/category): Forgetful functors preserve filtered colimits (#9101)

justus-springer committed 4 years ago

dc5a3db9

chore(analysis/special_functions): typo in module doc (#9330)

kim-em committed 4 years ago

41414a3a

feat(linear_algebra/matrix/basis): add matrix basis change formula (#9280)

riccardobrasca committed 4 years ago

2b84c4c6

feat(number_theory): the class group of an integral closure is finite (#9059)

Vierkantor committed 4 years ago

68dbf27c

chore(measure_theory/integral/set_integral): generalize, golf (#9328)

urkud committed 4 years ago

a5d2dbc5

chore(data/complex/module): rename `complex.smul_coe` to `real_smul` (#9326)

urkud committed 4 years ago

a994071f

feat(category_theory/*): Fully faithful functors induces equivalence (#9322)

erdOne committed 4 years ago

7e350c24

chore(analysis/convex): trivial generalizations of ℝ (#9298)

kim-em committed 4 years ago

15730e8d

feat(data/{list,multiset}): add `can_lift` instances (#9262)

urkud committed 4 years ago

eb3d6001

chore(measure_theory): add 2 lemmas (#9329)

urkud committed 4 years ago

c9638b97

chore(order/lattice): tidy up pi instances (#9305)

eric-wieser committed 4 years ago

6f2cbde0

feat(linear_algebra/std_basis): add matrix.std_basis_eq_std_basis_matrix (#9216)

riccardobrasca committed 4 years ago

f95f216f

chore(analysis/calculate/fderiv): move results about analytic functions to a new file (#9296)

kim-em committed 4 years ago

5b55a869

chore(*): removing unneeded imports (#9278)

kim-em committed 4 years ago

6d866224

feat(linear_algebra/affine_space/affine_subspace): prove that a set whose affine span is top cannot be empty. (#9113)

ocfnash committed 4 years ago

b77aa3aa

chore(data/complex/exponential): add `abs_exp`, golf (#9327)

urkud committed 4 years ago

f59dbf2c

feat(set_theory/cardinal_ordinal): mul_le_max and others (#9269)

ChrisHughes24 committed 4 years ago

7112730d

chore(linear_algebra/basic): generalize `add_monoid_hom_lequiv_{nat,int}` (#9233)

eric-wieser committed 4 years ago

9c34e80c

refactor(algebra/module/linear_map): Put linear equivalences in their own file (#9301)

eric-wieser committed 4 years ago

5625ec02

feat(analysis/normed_space/basic): the rescaling of a ball is a ball (#9297)

sgouezel committed 4 years ago

e0d568e5

chore(algebra/algebra/basic): remove a duplicate instance (#9320)

eric-wieser committed 4 years ago

56a6ed6e

Older