leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 5 years ago

10ef3657

kim-em committed 5 years ago

fb810784

chore(data/polynomial): missing a simp attribute (#3381)

kim-em committed 5 years ago

792faaed

chore(tactic/show_term): use Try this: (#3374)

kim-em committed 5 years ago

afa534cd

kim-em committed 5 years ago

b476232b

chore(data/nat/prime): @[pp_nodot] nat.prime (#3379)

kim-em committed 5 years ago

eb851ae2

Merge branch 'prime_pp_nodot' into 20200713_infinitude_of_primes

kim-em committed 5 years ago

c476f1cd

chore(data/nat/prime): @[pp_nodot] nat.prime

kim-em committed 5 years ago

f9d59d32

Merge remote-tracking branch 'origin/master' into 20200713_infinite_of_primes

kim-em committed 5 years ago

1c672512

feat(algebra/category/AddCommGroup): has_image_maps (#3366)

kim-em committed 5 years ago

a8d6bdf6

kim-em committed 5 years ago

8c522225

feat(data/polynomial): simp lemmas for bit0 / bit1 (#3376)

pglutz committed 5 years ago

fa6c45a8

feat(geometry/manifold/charted_space): typeclass `closed_under_restriction` for structure groupoids (#3347)

hrmacbeth committed 5 years ago

4e603f4b

Merge branch 'show_term_Try_this' into 20200713_infinite_of_primes

kim-em committed 5 years ago

966cbad9

chore(tactic/show_term): use Try this:

kim-em committed 5 years ago

93d9c4a1

kim-em committed 5 years ago

68b1dd0d

feat(algebra/add_torsor): more cancellation lemmas (#3368)

jsm28 committed 5 years ago

0e1c2bc4

kim-em committed 5 years ago

0ba2e31c

feat(data/set/finite): add a version of `prod_preimage` for `inj_on` (#3342)

urkud committed 5 years ago

b0473968

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

leanprover-community-bot committed 5 years ago

298caa08

feat(data/fintype/basic): set.to_finset_empty (#3361)

cfbolz committed 5 years ago

d7ac180f

chore(category_theory/comma): split into three files (#3358)

kim-em committed 5 years ago

34d3fe1d

refactor(tactic/push_neg): simp ¬ (p ∧ q) better (#3362)

digama0 committed 5 years ago

f742a3d6

feat(algebra/category/*): get rid of the local reducible hack (#3354)

kim-em committed 5 years ago

36a25d9f

feat(category/has_shift): missing simp lemmas (#3365)

kim-em committed 5 years ago

75b9cfa3

chore(category_theory/functor): explain how to type 𝟭 (#3364)

kim-em committed 5 years ago

f669a780

feat(tactic/interval_cases): add `with h` option (#3353)

shingtaklam1324 committed 5 years ago

574dac55

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

leanprover-community-bot committed 5 years ago

5ddbdc18

feat(interactive_expr): bigger accomplishment (#3359)

PatrickMassot committed 5 years ago

1aff3aff

feat(data/univariate/qpf): compositional data type framework for (co)inductive types (#3325)

cipher1024 committed 5 years ago

960fc8e3

Older