leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' of https://github.com/leanprover-community/mathlib into clifford_algebra

utensil committed 5 years ago

f33ce314

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

feat(analysis/special_functions/trigonometric): Added lemma cos_ne_zero_iff (#3743)

benjamindavidson committed 5 years ago

b1e56a21

chore(data/finset/order): use `[nonempty]` in `directed.finset_le` (#3759)

urkud committed 5 years ago

ced74696

chore(data/fintype/card): add `prod_bool` (#3758)

urkud committed 5 years ago

4c24a091

chore(data/fintype/card): DRY using `@... (multiplicative _)` (#3756)

urkud committed 5 years ago

31a0258b

feat(analysis/calculus/fderiv): multiplication by a complex respects real differentiability (#3731)

sgouezel committed 5 years ago

cc6528e7

feat(data/list/palindrome): define palindromes (#3729)

lambda-fairy committed 5 years ago

cfcbea6e

feat(algebra/order): more lemmas for projection notation (#3753)

fpvandoorn committed 5 years ago

c503b7af

fix(algebra/field) remove `one_div_eq_inv` (#3749)

fpvandoorn committed 5 years ago

6c8b2cd6

feat(tactic/clear_value): preserve order and naming (#3700)

cipher1024 committed 5 years ago

d6ffc1ad

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

leanprover-community-bot committed 5 years ago

cacb54ec

feat(tactic/choose): `choose` can now decompose conjunctions (#3699)

cipher1024 committed 5 years ago

486830b0

feat(tactic/rcases): type ascriptions in rcases (#3730)

digama0 committed 5 years ago

f8c81351

Older