leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/add_torsor): a few more lemmas and implicit args (#2964)

urkud committed 5 years ago

d18061fb

feat(analysis/special_functions/pow): rpow is differentiable (#2930)

sgouezel committed 5 years ago

1b2048d7

fix(tactic/squeeze_simp): make `squeeze_simp [←...]` work (#2961)

Vierkantor committed 5 years ago

5c851bdb

feat(analysis/special_functions/pow): real powers on ennreal (#2951)

sgouezel committed 5 years ago

a433eb07

feat(data/set/intervals/image_preimage): new file (#2958)

urkud committed 5 years ago

fd623d6c

feat(linear_algebra/quadratic_form): more constructions for quadratic forms (#2949)

Vierkantor committed 5 years ago

1ef65c99

feat(data/int|nat/basic): add `add_monoid_hom.ext_nat/int` (#2957)

urkud committed 5 years ago

31ceb624

feat(algebra/add_torsor): add `equiv.const_vadd` and `equiv.vadd_const` (#2907)

urkud committed 5 years ago

edb4422a

feat(topology/algebra/ordered): list of preconnected sets (#2943)

urkud committed 5 years ago

a130c73a

chore(algebra/group_power): simplify a proof (#2955)

urkud committed 5 years ago

8f89bd83

chore(algebra/*): merge `inv_inv''` with `inv_inv'` (#2954)

urkud committed 5 years ago

d7fa4051

feat(group_theory/subgroup): define normal bundled subgroups (#2947)

ChrisHughes24 committed 5 years ago

81618883

feat(data/setoid/partition): some lemmas about partitions (#2937)

ChrisHughes24 committed 5 years ago

2131382b

chore(analysis/convex/basic): add `finset.convex_hull_eq` (#2956)

urkud committed 5 years ago

80a52e99

feat(analysis/convex): preparatory statement for caratheodory (#2944)

kim-em committed 5 years ago

2ceb7f7f

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

leanprover-community-bot committed 5 years ago

beb5d45c

chore(is_ring_hom): remove some uses of is_ring_hom (#2884)

kim-em committed 5 years ago

1a297969

feat(topology/metric_space/isometry): group structure on isometries (#2950)

Matěj G committed 5 years ago

7d803a98

feat(ring/localization): add construction of localization as a quotient type (#2922)

101damnations committed 5 years ago

add0c9a8

feat(ring_theory/eisenstein_criterion): Eisenstein's criterion (#2946)

ChrisHughes24 committed 5 years ago

2dbf5508

refactor(data/zmod): generalize zmod.cast_hom (#2900)

jcommelin committed 5 years ago

c2e78d27

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

leanprover-community-bot committed 5 years ago

e397b4c1

chore(*): fix some `ge_or_gt` lint issues (#2945)

urkud committed 5 years ago

5744f897

refactor(analysis/specific_limits): prove `0 < r → (1+r)^n→∞` for semirings (#2935)

urkud committed 6 years ago

ef6d8d9e

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

leanprover-community-bot committed 6 years ago

1adf2041

chore(category_theory/limits/over): granularity in forget preserving colimits (#2941)

b-mehta committed 6 years ago

494b43ef

feat(category_theory/limits): dualise a limits result (#2940)

b-mehta committed 6 years ago

97265f9c

feat(data/fintype/basic): to_finset_inj (#2938)

ChrisHughes24 committed 6 years ago

e2052286

feat(topology/algebra/ordered): IVT for two functions (#2933)

urkud committed 6 years ago

74037cba

chore(tactic/localized): lower priority of bad decidability instances in classical locale (#2932)

sgouezel committed 6 years ago

f44509c0

Newer Older