leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/yoneda): better simp lemmas for small yoneda (#4743)

b-mehta committed 5 years ago

f2793132

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

leanprover-community-bot committed 5 years ago

8bd1df59

chore(data/polynomial): remove monomial_one_eq_X_pow (#4734)

faenuccio committed 5 years ago

de12036b

chore(data/equiv/basic): Add a simp lemma perm.coe_mul (#4723)

eric-wieser committed 5 years ago

6eb55641

chore(*): 3 unrelated small changes (#4732)

urkud committed 5 years ago

add50960

feat(algebra/monoid_algebra): define a non-commutative version of `lift` (#4725)

urkud committed 5 years ago

aba31c93

feat(linear_algebra/nonsingular_inverse): state Cramer's rule explicitly (#4700)

Oliver Nash committed 5 years ago

fb5ef2b9

refactor(algebra/add_torsor): define pointwise `-ᵥ` and `+ᵥ` on sets (#4710)

urkud committed 5 years ago

03f0285d

feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structures from partial information (#4664)

awainverse committed 5 years ago

4c4d47c2

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

leanprover-community-bot committed 5 years ago

fca876ea

feat(archive): formalize compiler correctness by McCarthy and Painter (#4702)

xiw committed 5 years ago

df450024

feat(linear_algebra/affine_space): define `affine_equiv` (#2909)

urkud committed 5 years ago

1b4e7694

chore(linear_algebra/basic): a few simp lemmas (#4727)

urkud committed 5 years ago

75316cad

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

leanprover-community-bot committed 5 years ago

01c1e6fb

fixup(category_theory/sites): add arrow sets that aren't sieves (#4703)

b-mehta committed 5 years ago

3a860cc4

chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717)

b-mehta committed 5 years ago

857cbd52

feat(data/complex/module): ![1, I] is a basis of C over R (#4713)

urkud committed 5 years ago

8489972a

chore(*): review some lemmas about injectivity of coercions (#4711)

urkud committed 5 years ago

cf551ee3

chore(.gitignore): gitignore for emacs temp files (#4699)

lacker committed 5 years ago

5d52ea42

fix(tactic/norm_num): remove one_div from simp set (#4705)

digama0 committed 5 years ago

8131349c

feat(linear_algebra/affine_space/ordered): define `slope` (#4669)

urkud committed 5 years ago

617e8295

chore(data/finsupp): minor review (#4712)

urkud committed 5 years ago

b46190f9

chore(data/polynomial): slightly generalize `map_eq_zero` and `map_ne_zero` (#4708)

urkud committed 5 years ago

288802b6

chore(topology/algebra/ordered): drop section vars, golf 2 proofs (#4706)

urkud committed 5 years ago

21415c8c

chore(data/set): a few more lemmas about `image2` (#4695)

urkud committed 5 years ago

0cf8a98b

feat(data/real/pi): Leibniz's series for pi (#4228)

hrmacbeth committed 5 years ago

050b5a1b

feat(measure_theory): finite_spanning_sets_in (#4668)

fpvandoorn committed 5 years ago

cd884eb8

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

leanprover-community-bot committed 5 years ago

9755ae3c

chore(data/finsupp): `to_additive` on `on_finset_sum` (#4698)

urkud committed 5 years ago

accc50ed

chore(data/multiset): add a few lemmas (#4697)

urkud committed 5 years ago

706b4841

Newer Older