leanprover-community/mathlib3

Pull Requests Commits

feat(*): has_mem (set α) (filter α) (#799)

Patrick Massot committed 6 years ago

ffa6d699

refactor(localization): shorten proofs (#796)

ChrisHughes24 committed 6 years ago

7e779677

feat(data/list): lemmas about count and bag_inter (#797)

kim-em committed 6 years ago

26bd400b

feat(tactic/basic): utility functions for names (#791)

kim-em committed 6 years ago

181647bb

feat(algebra/group): units.coe_map

ChrisHughes24 committed 6 years ago

Verified 48eaf05b

feat(data/nat/basic): some lemmas (#792)

kim-em committed 6 years ago

e286452d

feat(data/finset): missing fold_map lemma (#794)

kim-em committed 6 years ago

61e02dd2

feat(ring_theory/localization): adds induced ring hom between fraction rings (#781)

jcommelin committed 6 years ago

cc753d7b

fix(tactic/linarith): correctly parse 0*0

robertylewis committed 6 years ago

1ec0a1f4

feat(topology): split uniform_space and topological_structure

PatrickMassot committed 6 years ago

581cf19b

feat(data/multiset): add monad instance (#744)

kckennylau committed 6 years ago

708c0cfa

refactor(topology/metric_space/lipschitz): Simplify proof in banach contraction (#788)

sgouezel committed 6 years ago

3525d212

feat(data/finset): add card_sdiff

johoelzl committed 6 years ago

b9f88d14

feat(linear_algebra): module (vector space) structure for finsupp, matrix, and mv polynomials

johoelzl committed 6 years ago

682f4b5a

feat(data/matrix): basic definitions: transpose; row & column matrix; vector/matrix multiplication

johoelzl committed 6 years ago

738778aa

refactor(linear_algebra): move multivariate_polynomial to data

johoelzl committed 6 years ago

528ff933

refactor(ring_theory): move matrix to data and determinant to linear_algebra

johoelzl committed 6 years ago

891a192f

feat(linear_algebra): add module (vector_space) structure for function spaces

johoelzl committed 6 years ago

10a586b1

feat(data/fintype): card_univ and card_univ_diff

johoelzl committed 6 years ago

332121d4

refactor(data/finset): correct name sdiff_disjoint -> disjoint_sdiff; add sdiff_disjoint

johoelzl committed 6 years ago

c0b1eb19

remove superflous parameter from bot_eq_zero

johoelzl committed 6 years ago

b3c749b4

feat(data/finset): add filter_empty, filter_subset_filter, prod_filter

johoelzl committed 6 years ago

73f1a08d

feat(data/finset): add disjoint_bind_left/right

johoelzl committed 6 years ago

b9ead4d5

refactor(algebra): canonically_ordered_monoid extends order_bot

johoelzl committed 6 years ago

f82f5f2a

feat(data/equiv): add subtype_pi_equiv_pi

johoelzl committed 6 years ago

f07a558d

feat(data/set/lattice): more rules for disjoint sets

johoelzl committed 6 years ago

8070c05c

feat(data/set): relate range and image to Union

johoelzl committed 6 years ago

c53ac415

feat(data/set): add exists_maximal_wrt

johoelzl committed 6 years ago

41038bac

feat(data/set): add finite_image_iff_on

johoelzl committed 6 years ago

146d73c6

feat(data/set): add subset_image_iff and subset_range_iff

johoelzl committed 6 years ago

84a5f4d3

Newer Older