leanprover-community/mathlib

Pull Requests Commits

refactor(order/atoms): reorder arguments of `is_simple_lattice.fintype` (#8933)

fpvandoorn committed 5 years ago

1dbd561f

feat(algebra/module/prod,pi): instances for actions with zero (#8929)

pechersky committed 5 years ago

22a297ca

chore(measure_theory/*): rename `probability_measure` and `finite_measure` (#8831)

hrmacbeth committed 5 years ago

f4d72050

feat(topology/algebra/ordered): monotone convergence in pi types (#8841)

urkud committed 5 years ago

6adb5e8b

chore(algebra/direct_sum/algebra): add missing rfl lemmas (#8924)

eric-wieser committed 5 years ago

4a65197a

fix(data/set/finite): drop {α : Type}, fixes universe issue (#8922)

jcommelin committed 5 years ago

aa0694a1

doc(tactic/lint): instructions on fails_quickly failure (#8910)

fpvandoorn committed 5 years ago

ad7519a3

chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)

urkud committed 5 years ago

b3807ee3

chore(algebra/monoid_algebra): convert a filename prefix into a folder (#8925)

eric-wieser committed 5 years ago

1e89df22

feat(algebra/direct_sum): graded algebras (#8783)

eric-wieser committed 5 years ago

98466d29

fix(ring_theory/polynomial/homogeneous): spelling mistake in `homogeneous` (#8914)

eric-wieser committed 5 years ago

2bae06af

feat(algebraic_geometry): Lift isomorphism of sheafed spaces to locally ringed spaces (#8887)

justus-springer committed 5 years ago

395bb6ca

refactor(data/set/finite): use `[fintype (plift ι)]` in `finite_Union` (#8872)

urkud committed 5 years ago

d75a2d96

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

tb65536 committed 5 years ago

db06b5a2

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

justus-springer committed 5 years ago

e824b88d

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

kmill committed 5 years ago

14a992b3

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

ineswright committed 5 years ago

0b485703

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

kex-y committed 5 years ago

1aaff8da

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

pechersky committed 5 years ago

42b5e801

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

YaelDillies committed 5 years ago

8ee05e9a

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

leanprover-community-bot committed 5 years ago

d3c592f0

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

FrickHazard committed 5 years ago

0fd51b1c

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

Vierkantor committed 5 years ago

2eaec057

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

pechersky committed 5 years ago

c4cf4c25

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

Vierkantor committed 5 years ago

dcd60e25

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

shadasali committed 5 years ago

7f256987

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

kex-y committed 5 years ago

7cfc9872

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

Vierkantor committed 5 years ago

023a816d

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

Vierkantor committed 5 years ago

a3278519

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

pechersky committed 5 years ago

88e47d7c

Newer Older