leanprover-community/mathlib

Pull Requests Commits

chore(ring_theory/adjoin/basic): golf some proofs about algebra.adjoin (#6784)

eric-wieser committed 5 years ago

df4c9c95

chore(topology/metric_space): add '@[continuity]' attributes (#6780)

kim-em committed 5 years ago

9f77db21

refactor(algebraic_topology/simplex_category): Make simplex_category universe polymorphic. (#6761)

adamtopaz committed 5 years ago

695d7f4f

refactor(category_theory/cones): golf and cleanup cones (#6756)

b-mehta committed 5 years ago

4db82a40

feat(category_theory/closed): currying rfl lemmas (#6754)

b-mehta committed 5 years ago

56e5aa74

fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778)

benjamindavidson committed 5 years ago

b0150a5d

feat(topology): continuous_pi_iff pi.has_continuous_mul pi.topological_group (#6689)

agjftucker committed 5 years ago

26fcfbc9

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

leanprover-community-bot committed 5 years ago

07282da6

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

urkud committed 5 years ago

b4a2991c

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

winston-h-zhang committed 5 years ago

eba4829b

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

pechersky committed 5 years ago

c65146d6

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

urkud committed 5 years ago

2d2929f8

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

thejohncrafter committed 5 years ago

152412ff

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

thejohncrafter committed 5 years ago

6f3e0ad1

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

eric-wieser committed 5 years ago

591c34b6

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

benjamindavidson committed 5 years ago

ce107da5

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

kim-em committed 5 years ago

590f43db

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

mo271 committed 5 years ago

c1701287

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

tb65536 committed 5 years ago

86e1b175

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

b-mehta committed 5 years ago

62d532a7

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

leanprover-community-bot committed 5 years ago

a1305bea

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

kim-em committed 5 years ago

cc11e44c

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

urkud committed 5 years ago

c3e40bef

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

tb65536 committed 5 years ago

02f77ab9

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

adomani committed 5 years ago

aea7dfbc

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

pechersky committed 5 years ago

a10bc3d3

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

eric-wieser committed 5 years ago

e1ff2dff

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

eric-wieser committed 5 years ago

83b0981b

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

kim-em committed 5 years ago

744d59af

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

kim-em committed 5 years ago

58581d0f

Newer Older