leanprover-community/mathlib

Pull Requests Commits

intro new simp lemma

jalex-stark committed 5 years ago

7da0ca59

jalex-stark committed 5 years ago

91954fef

chore(number_theory/pythagorean_triples): added doc-strings (#3787)

JamesAMaths committed 5 years ago

daafd6f7

feat(algebra/add_torsor): injectivity lemmas (#3767)

jsm28 committed 5 years ago

10d4811e

chore(algebra/classical_lie_algebras): fix some doc strings (#3776)

Oliver Nash committed 5 years ago

5c13693f

refactor(set_theory/pgame): rename pgame lemma (#3775)

foxthomson committed 5 years ago

9ac6e8ad

feat(tactic/derive_fintype): derive fintype instances (#3772)

digama0 committed 5 years ago

658cd387

feat(analysis/special_functions/pow): Added lemmas for rpow of neg exponent (#3715)

benjamindavidson committed 5 years ago

18746ef6

feat(topology/sheaves): the sheaf condition (#3605)

kim-em committed 5 years ago

099f070f

refactor(algebra/add_torsor): use `out_param` (#3727)

urkud committed 5 years ago

36b4a1e3

feat(data/nat/basic): one mod two or higher is one (#3763)

pechersky committed 5 years ago

2b8ece64

Revert "chore(ring_theory): delete `is_algebra_tower`"

Vierkantor committed 5 years ago

c444a005

chore(ring_theory): delete `is_algebra_tower`

Vierkantor committed 5 years ago

c956ce15

feat(control/equiv_functor): fintype instance (#3783)

kim-em committed 5 years ago

67dad7f3

fix(tactic/apply): fix ordering of goals produced by `apply` (#3777)

cipher1024 committed 5 years ago

b670212c

refactor(data/list/tfae): tfae.out (#3774)

digama0 committed 5 years ago

c1a5283b

fix(algebra/archimedean): switch to a more natural and general condition in exists_nat_pow_near (#3782)

alreadydone committed 5 years ago

55f49265

fix(tactic/equiv_rw): fix problem with stuck universe metavariables (#3773)

kim-em committed 5 years ago

3ae44bd1

chore(*): use notation for `filter.prod` (#3768)

urkud committed 5 years ago

c2528003

chore(*): assorted lemmas for FTC-1 (#3755)

urkud committed 5 years ago

0e5f44b0

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

leanprover-community-bot committed 5 years ago

b611c5fa

feat(ci): auto label merge conflicts, try 2 (#3766)

robertylewis committed 5 years ago

32c6a73e

feat(tactic/find_unused): find the dead code in a module (#3701)

cipher1024 committed 5 years ago

627b4317

feat(ideals,submonoids,subgroups): mem_sup(r) and mem_inf(i) lemmas (#3697)

ChrisHughes24 committed 5 years ago

28dfad8c

chore(data/int/basic): norm_cast attribute on int.coe_nat_mod (#3765)

ChrisHughes24 committed 5 years ago

4cc094bc

feat(intervals/image_preimage): preimage under multiplication (#3757)

urkud committed 5 years ago

c66ecd3f

feat(ci): auto label merge conflicts (#3761)

robertylewis committed 5 years ago

f912f188

refactor(algebra/associated): change several instances from [integral_domain] to [comm_cancel_monoid_with_zero] (#3744)

awainverse committed 5 years ago

34352c2d

feat(data/polynomial): adds map_comp (#3736)

pglutz committed 5 years ago

2c4300b4

feat(data/*): Add sizeof lemmas. (#3745)

DanielFabian committed 5 years ago

ac2f0118

Older