leanprover-community/mathlib

Pull Requests Commits

doc(tactic/localized): unnecessary escape characters (#3322)

robertylewis committed 5 years ago

afae2c4b

refactor(category_theory/finite_limits): reorganise import hierarchy (#3320)

kim-em committed 5 years ago

18246ac4

chore(category_theory/images): cleanup (#3314)

kim-em committed 5 years ago

13eea4c3

feat(data/int/basic): some lemmas (#3313)

kim-em committed 5 years ago

eb271b26

feat(data/equiv): α × α ≃ α for [subsingleton α] (#3312)

kim-em committed 5 years ago

ff1aea54

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

leanprover-community-bot committed 5 years ago

e987f625

feat(topology/metric_space/basic): add closed_ball_mem_nhds (#3305)

kbuzzard committed 5 years ago

23f449bd

feat(linear_algebra/finite_dimensional): add dim_sup_add_dim_inf_eq (#3304)

kbuzzard committed 5 years ago

35940dda

feat(data/list/defs): list.singleton_append and list.bind_singleton (#3298)

lambda-fairy committed 5 years ago

ea10944c

chore(algebra/big_operators): use proper `*_with_zero` class in `prod_eq_zero(_iff)` (#3303)

urkud committed 5 years ago

11ba6873

feat(algebra/continued_fractions): add first set of approximation lemmas (#3218)

kappelmann committed 5 years ago

12c2acb8

feat(analysis/normed_space/operator_norm): normed algebra of continuous linear maps (#3282)

hrmacbeth committed 5 years ago

08ffbbb9

refactor(order/*): make `data.set.basic` import `order.bounded_lattice` (#3285)

urkud committed 5 years ago

095445ee

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

leanprover-community-bot committed 5 years ago

d62e71d4

feat(linear_algebra/affine_space): lattice structure on affine subspaces (#3288)

jsm28 committed 5 years ago

f548db40

chore(ring_theory/power_series): weaken assumptions for nontrivial (#3301)

sgouezel committed 5 years ago

edd29d0f

chore(*): update to lean 3.17.0 (#3300)

gebner committed 5 years ago

c0926f06

feat(data/sym2) Defining the symmetric square (unordered pairs) (#3264)

kmill committed 5 years ago

f06e4e00

feat(tactic/interactive): identity tactic (#3295)

digama0 committed 5 years ago

e3a1a619

refactor(*): replace nonzero with nontrivial (#3296)

sgouezel committed 5 years ago

33b6cba0

chore(scripts/nolints_summary.sh): list number of nolints per file

jcommelin committed 5 years ago

2c9d9bd0

feat(topology): preliminaries for Haar measure (#3194)

fpvandoorn committed 5 years ago

5ff099b6

refactor(algebra/inj_surj): more lemmas, move to files, rename (#3290)

urkud committed 5 years ago

2e140f1e

fix(finset/lattice): undo removal of bUnion_preimage_singleton (#3293)

fpvandoorn committed 5 years ago

ffa504c9

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

leanprover-community-bot committed 5 years ago

e1f6ed23

doc(tactic/explode): expand doc string (#3271)

bryangingechen committed 5 years ago

0cd500ef

chore(category_theory/over/limits): change instance to def (#3281)

b-mehta committed 5 years ago

293287d5

chore(algebra/category): use preadditivity for biproducts (#3280)

TwoFX committed 5 years ago

f39e0d7a

feat(ring_theory/localization): order embedding of ideals, local ring instance (#3287)

101damnations committed 5 years ago

023d4f7d

feat(data/pnat): basic pnat facts needed for perfect numbers (3094) (#3274)

awainverse committed 5 years ago

08e1adc8

Newer Older