leanprover-community/mathlib3

Pull Requests Commits

feat(data/list/fibword): Fibonacci words

lambda-fairy committed 5 years ago

b303606b

feat(data/list/fibword): Fibonacci words

lambda-fairy committed 5 years ago

efd76b2a

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

feat(.): add code of conduct (#3747)

robertylewis committed 5 years ago

4324778f

feat(field_theory/algebraic_closure): algebraic closure (#3733)

kckennylau committed 5 years ago

eb4b2a05

feat(topology/opens): open_embedding_of_le (#3597)

kim-em committed 5 years ago

bfcf6400

docs(category/default): Fix typo for monomorphism (#3741)

utensil committed 5 years ago

06e14052

refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714)

awainverse committed 5 years ago

f92fd0d1

feat(haar_measure): define the Haar measure (#3542)

fpvandoorn committed 5 years ago

57df7f5a

Older