leanprover-community/mathlib3

Pull Requests Commits

fpvandoorn committed 4 years ago

9c1e8853

chore(order/bounded_lattice): dot-notation lemmas ne.bot_lt and ne.lt_top (#8935)

jcommelin committed 4 years ago

3d6a8285

chore(topology/metric_space/basic): add `metric.uniform_continuous_on_iff_le` (#8906)

urkud committed 4 years ago

12bbd533

feat(measure_theory/hausdorff_measure): dimH and Hölder/Lipschitz maps (#8361)

urkud committed 4 years ago

603a6066

chore(group_theory/submonoid/center): fix typo and extend docstring (#8937)

eric-wieser committed 4 years ago

d9b2db99

feat(group_theory/submonoid): center of a submonoid (#8921)

eric-wieser committed 4 years ago

ab967d23

fix(order/rel_classes): remove looping instance (#8931)

fpvandoorn committed 4 years ago

6b63c034

fix(data/complex/basic): better formulas for nsmul and gsmul on complex to fix a diamond (#8928)

sgouezel committed 4 years ago

53f074ca

feat(logic/basic): equivalence of by_contra and choice (#8912)

digama0 committed 4 years ago

c04e8a48

feat(algebraic_geometry): Restriction of locally ringed spaces (#8809)

justus-springer committed 4 years ago

1c134548

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

fpvandoorn committed 4 years ago

1dbd561f

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

pechersky committed 4 years ago

22a297ca

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

hrmacbeth committed 4 years ago

f4d72050

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

urkud committed 4 years ago

6adb5e8b

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

eric-wieser committed 4 years ago

4a65197a

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

jcommelin committed 4 years ago

aa0694a1

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

fpvandoorn committed 4 years ago

ad7519a3

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

urkud committed 4 years ago

b3807ee3

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

eric-wieser committed 4 years ago

1e89df22

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

eric-wieser committed 4 years ago

98466d29

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

eric-wieser committed 4 years ago

2bae06af

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

justus-springer committed 4 years ago

395bb6ca

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

urkud committed 4 years ago

d75a2d96

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

Older