leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 4 years ago

07282da6

feat(dynamics/ergodic): define measure preserving maps (#6764)

urkud committed 4 years ago

b4a2991c

feat(data/real/pi): Wallis product for pi (#6568)

winston-h-zhang committed 4 years ago

eba4829b

chore(data/finset/basic): erase_inj_on (#6769)

pechersky committed 4 years ago

c65146d6

feat(measure_theory): define Hausdorff measure and Hausdorff dimension (#6710)

urkud committed 4 years ago

2d2929f8

feat(analysis/special_functions/exp_log): log_nonzero_of_ne_one and log_inj_pos (#6734)

thejohncrafter committed 4 years ago

152412ff

feat(ring_theory/multiplicity): Multiplicity with units (#6729)

thejohncrafter committed 4 years ago

6f3e0ad1

refactor(linear_algebra/basic): move the lattice structure to its own file (#6767)

eric-wieser committed 4 years ago

591c34b6

feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597)

benjamindavidson committed 4 years ago

ce107da5

docs(category_theory): missing module docs (#6752)

kim-em committed 4 years ago

590f43db

feat(number_theory/bernoulli): faulhaber' (#6684)

mo271 committed 4 years ago

c1701287

feat(field_theory/abel_ruffini): solvable by radicals implies solvable Galois group (#6631)

tb65536 committed 4 years ago

86e1b175

feat(data/finset): erase is partially injective (#6737)

b-mehta committed 4 years ago

62d532a7

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

leanprover-community-bot committed 4 years ago

a1305bea

ci(*): lint 'Authors: ' line (#6750)

kim-em committed 4 years ago

cc11e44c

feat(data/equiv/local_equiv): define `piecewise` and `disjoint_union` (#6700)

urkud committed 4 years ago

c3e40bef

doc(field_theory/normal): Add authors (#6759)

tb65536 committed 4 years ago

02f77ab9

chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ (#6753)

adomani committed 4 years ago

aea7dfbc

feat(normed_space/inner_product): euclidean_space.norm_eq (#6744)

pechersky committed 4 years ago

a10bc3d3

chore(*): update `injective` lemma names to match the naming guide (#6740)

eric-wieser committed 4 years ago

e1ff2dff

feat(ring_theory/polynomial): the symmetric and homogenous polynomials form a subalgebra and submodules, respectively (#6666)

eric-wieser committed 4 years ago

83b0981b

refactor(category_theory/limits): split file (#6751)

kim-em committed 4 years ago

744d59af

chore(*): normalize Authors: line (#6749)

kim-em committed 4 years ago

58581d0f

refactor(algebra/algebra/basic): change submodule.restrict_scalars to use is_scalar_tower (#6745)

eric-wieser committed 4 years ago

542ff6af

feat(algebra/associated): Primes that divide each other are associated (#6732)

thejohncrafter committed 4 years ago

59cda3bb

feat(ring_theory/principal_ideal_domain): The generator of a principal prime ideal is a prime (#6731)

thejohncrafter committed 4 years ago

db2a972d

feat(data/padics/padic_norm): p-adic norm of primes other than p (#6730)

thejohncrafter committed 4 years ago

b4afd642

feat(group_theory/quaternion_group): define the (generalised) quaternion groups (#6683)

Julian-Kuelshammer committed 4 years ago

216aecd7

doc(category_theory): convert comments about universes to library note (#6748)

kim-em committed 4 years ago

8116851f

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

leanprover-community-bot committed 4 years ago

e955a6bd

Newer Older