leanprover-community/mathlib

Pull Requests Commits

chore(category/equivalence): cleanup (#3164)

kim-em committed 5 years ago

266d3163

feat(category/preadditive): comp_sum (#3162)

kim-em committed 5 years ago

e8187ac1

feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148)

urkud committed 5 years ago

3875012a

feat(algebra/big_operators): prod_dite_eq (#3167)

kim-em committed 5 years ago

553e4534

refactor(algebra/*): small API fixes (#3157)

urkud committed 5 years ago

8f04a92a

feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres (#3074)

b-mehta committed 5 years ago

e1a72b50

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

leanprover-community-bot committed 5 years ago

5c7e1a22

chore(algebra/ordered_group): merge `add_le_add'` with `add_le_add` (#3159)

urkud committed 5 years ago

2aa08c1f

feat(linear_algebra/finsupp_vector_space): is_basis.tensor_product (#3147)

kckennylau committed 5 years ago

04a5bdbc

refactor(tactic/linarith): big refactor and docs (#3113)

robertylewis committed 5 years ago

dd9b5c68

feat(ring_theory/localization): integral closure in field extension (#3096)

Vierkantor committed 5 years ago

194edc12

feat(order/filter/countable_Inter): `sup` and `inf` (#3154)

urkud committed 5 years ago

8ecf53d9

feat(uniform_space/separation): add separated_set (#3130)

PatrickMassot committed 5 years ago

617b07e0

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

leanprover-community-bot committed 5 years ago

985cce7b

feat(field_theory/separable): definition and basic properties (#3155)

kckennylau committed 5 years ago

d57ac08c

refactor(geometry/manifold/*): rename to charted_space and tangent_map (#3103)

sgouezel committed 5 years ago

340d5a9d

chore(data/set/finite): use dot notation (#3151)

urkud committed 5 years ago

bc3ed51b

feat(topology/metric_space/baire): define filter `residual` (#3149)

urkud committed 5 years ago

26918a05

chore(linear_algebra/nonsingular_inverse): `matrix.nonsing_inv` no longer requires base ring to carry `has_inv` instance (#3136)

Oliver Nash committed 5 years ago

62e13643

fix(algebra/ordered*): add norm_cast attribute (#3132)

kbuzzard committed 5 years ago

ea665e7d

refactor(order/filter/basic): define `filter.eventually_eq` (#3134)

urkud committed 5 years ago

d287d345

chore(topology/metric_space/baire): review (#3146)

urkud committed 5 years ago

421ed703

chore(topology/metric_space/basic): rename `uniform_continuous_dist'` (#3145)

urkud committed 5 years ago

159766e9

perf(tactic/cache): call `freeze_local_instances` after `reset_instance_cache` (#3128)

gebner committed 5 years ago

02d880b0

refactor(group/perm) bundle sign of a perm as a monoid_hom (#3143)

alexjbest committed 5 years ago

c0d74a39

chore(algebra/ring,char_zero): generalize some lemmas (#3141)

urkud committed 5 years ago

23d61413

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

leanprover-community-bot committed 5 years ago

52abfcf5

feat(data/finset): add card_insert_of_mem (#3137)

kbuzzard committed 5 years ago

b5625759

chore(*): update to Lean 3.16.4c (#3139)

robertylewis committed 5 years ago

36e3b9f1

feat(order/complete_lattice): complete lattice of Sup (#3138)

b-mehta committed 5 years ago

67844a81

Newer Older