leanprover-community/mathlib

Pull Requests Commits

chore(data/fintype/basic): split, and reduce imports (#3319)

kim-em committed 5 years ago

27f622ef

chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299)

kckennylau committed 5 years ago

f90fcc9e

feat(ring_theory/polynomial_algebra): polynomial A ≃ₐ[R] (A ⊗[R] polynomial R) (#3275)

kim-em committed 5 years ago

ba8af8cb

feat(algebra/ordered_field): missing lemma (#3324)

robertylewis committed 5 years ago

8f6090ca

doc(tactic/lean_core_docs): remove "hypothesis management" tag (#3323)

robertylewis committed 5 years ago

97853b96

feat(category_theory/zero): lemmas about zero objects and zero morphisms, and improve docs (#3315)

kim-em committed 5 years ago

a3e21a88

refactor(*): place map_map in the functor namespace (#3309)

PatrickMassot committed 5 years ago

fbb49cbe

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

Older