leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

55dfac8f

Move content between files

eric-wieser committed 4 years ago

352acd8d

Merge branch 'eric-wieser/direct_sum_graded.algebra' into eric-wieser/free_algebra-grading

eric-wieser committed 4 years ago

aa2138e1

eric-wieser committed 4 years ago

5558fe8b

eric-wieser committed 4 years ago

d083a706

Use the new instance

eric-wieser committed 4 years ago

e64ff957

Review comments, replace a def with an instance

eric-wieser committed 4 years ago

365533cb

Merge remote-tracking branch 'origin/master' into eric-wieser/direct_sum_graded.algebra

eric-wieser committed 4 years ago

88cdcccb

feat(group_theory/perm/cycle_type): Fixed points of permutations of prime order (#8832)

tb65536 committed 4 years ago

db06b5a2

refactor(category_theory/limits/final): Symmetric API for final and initial functors (#8808)

justus-springer committed 4 years ago

e824b88d

chore(data/set_like): some additional documentation (#8765)

kmill committed 4 years ago

14a992b3

feat(group_theory/nilpotent): add subgroups of nilpotent group are nilpotent (#8854)

ineswright committed 4 years ago

0b485703

feat(measure_theory/decomposition/lebesgue): Lebesgue decomposition for sigma-finite measures (#8875)

kex-y committed 4 years ago

1aaff8da

feat(data/polynomial/basic): monomial_eq_zero_iff (#8897)

pechersky committed 4 years ago

42b5e801

feat(data/nat/log): Ceil log (#8764)

YaelDillies committed 4 years ago

8ee05e9a

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

leanprover-community-bot committed 4 years ago

d3c592f0

feat(data/real/irrational): exists irrational between any two distinct rationals and reals (#8753)

FrickHazard committed 4 years ago

0fd51b1c

feat(ring_theory): define integrally closed domains (#8893)

Vierkantor committed 4 years ago

2eaec057

feat(algebra/polynomial/big_operators): coeff of sums and prods of polynomials (#8680)

pechersky committed 4 years ago

c4cf4c25

feat(ring_theory/trace): the trace form is nondegenerate (#8777)

Vierkantor committed 4 years ago

dcd60e25

feat(analysis/complex/isometry): Show that certain complex isometries are not equal (#8646)

shadasali committed 4 years ago

7f256987

feat(measure_theory/decomposition/radon_nikodym): the Radon-Nikodym theorem (#8763)

kex-y committed 4 years ago

7cfc9872

feat(algebra): define a bundled type of absolute values (#8881)

Vierkantor committed 4 years ago

023a816d

feat(ring_theory): a typeclass `is_integral_closure` (#8882)

Vierkantor committed 4 years ago

a3278519

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux (#8681)

pechersky committed 4 years ago

88e47d7c

refactor(*): use `is_empty` instead of `not (nonempty α)` (#8858)

urkud committed 4 years ago

0c503262

feat(category_theory/structured_arrow): Duality between structured and costructured arrows (#8807)

justus-springer committed 4 years ago

fe13f030

doc(ring_theory/hahn_series): Update Hahn Series docstring (#8883)

awainverse committed 4 years ago

4705a6b5

feat(algebra/big_operators/basic): add `prod_dite_of_false`, `prod_dite_of_true` (#8865)

ocfnash committed 4 years ago

a9de1979

feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878)

alexjbest committed 4 years ago

bcd5cd37

Older