leanprover-community/mathlib

Pull Requests Commits

Philip Wood committed 3 years ago

2098ad30

Final Result Proved

Philip Wood committed 3 years ago

94c3dbaf

Update maclaurin_sqrt_one_plus_x.lean

tyler-billingsley committed 3 years ago

76e51c50

Merge branch 'formal_power_series' of github.com:leanprover-community/mathlib into formal_power_series

tyler-billingsley committed 3 years ago

ff48c790

Update maclaurin_sqrt_one_plus_x.lean

tyler-billingsley committed 3 years ago

15c7ac0c

Working towards modified catalan descent lemma

Philip Wood committed 3 years ago

6fc42402

Catalan descent lemma proved

Philip Wood committed 3 years ago

54786dff

Really trying again

Philip Wood committed 3 years ago

efcfe719

Merge branch 'formal_power_series' of github.com:leanprover-community/mathlib into formal_power_series

Philip Wood committed 3 years ago

1b15f284

Philip Wood committed 3 years ago

43ff3d3e

Proves prop on Catalan power series squared

Philip Wood committed 3 years ago

6754d2e8

Cos identity, Start on Maclaurin

tyler-billingsley committed 3 years ago

914b6b41

gergg branch 'master' into formal_power_series

tyler-billingsley committed 3 years ago

08196263

tyler-billingsley committed 3 years ago

9b72fd51

tyler-billingsley committed 3 years ago

2531088e

This is n=1 and n=0 case for Catalan project

Philip Wood committed 3 years ago

9975ec74

This is n=1 case for Catalan project

Philip Wood committed 3 years ago

cab7e997

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

fpvandoorn committed 3 years ago

f7313156

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

fpvandoorn committed 3 years ago

25f60b46

feat(tactic/linear_combination): add parser for `h / a` (#15284)

digama0 committed 3 years ago

51f76d05

feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)

ericrbg committed 3 years ago

be53c7cb

feat(combinatorics/additive/behrend): Behrend's construction (#14070)

YaelDillies committed 3 years ago

44999a92

feat(set_theory/ordinal/basic): mark `type_fintype` as `simp` (#15194)

vihdzp committed 3 years ago

2084baf2

refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` (#15191)

eric-wieser committed 3 years ago

93e164e8

Merge branch 'formal_power_series' of github.com:leanprover-community/mathlib into formal_power_series

Philip Wood committed 3 years ago

d8201040

tyler-billingsley committed 3 years ago

bb8f8819

Merge branch 'master' into formal_power_series

Philip Wood committed 3 years ago

a1ffe9d1

This is 2/3 cos

Philip Wood committed 3 years ago

442773bb

Finished cosine identity

tyler-billingsley committed 3 years ago

9515e374

Merge branch 'formal_power_series' of github.com:leanprover-community/mathlib into formal_power_series

tyler-billingsley committed 3 years ago

6bd6345c

Older