leanprover-community/mathlib3

Pull Requests Commits

prove Z[i] is a euclidean_domain

ChrisHughes24 committed 6 years ago

49a85f48

refactor(*): move matrix.lean to data/ and determinant.lean to linear_algebra/ (#779)

jcommelin committed 6 years ago

1f4f2e42

feat(topology/metric_space/hausdorff_distance): Hausdorff distance

sgouezel committed 6 years ago

8fbf296d

feat(analysis/exponential): added inequality lemmas

callesonne committed 6 years ago

be88ceca

feat(group_theory): free_group and free_abelian_group are lawful monads (#737)

kckennylau committed 6 years ago

0bb0cec5

feat(data/zmod/basic): cast_mod_nat' and cast_mod_int' (#783)

ChrisHughes24 committed 6 years ago

Verified 116cffff

refactor(analysis/asymptotics): minor formatting changes

avigad committed 6 years ago

04b5f885

feat(analysis/normed_space/deriv): generalize to spaces over any normed field

avigad committed 6 years ago

6363212d

feat(analysis/normed_space/deriv): add readable proof of chain rule

avigad committed 6 years ago

89b8915e

feat(analysis/*): is_bigo -> is_O, is_littleo -> is_o

avigad committed 6 years ago

5dd1ba58

fix(*): fix things from change tendsto_congr -> tendsto.congr'

avigad committed 6 years ago

49ecc7b0

add has_fderiv_at_filter

digama0 committed 6 years ago

d74804bd

fix(asymptotics, deriv): minor formatting fixes

avigad committed 6 years ago

21b1fcc8

feat(analysis/asymptotics,analysis/normed_space/deriv): improvements and additions

avigad committed 6 years ago

16033bb5

feat(analysis/normed_space/deriv): start on derivative

avigad committed 6 years ago

6265d261

feat(analysis/asymptotics): start on bigo and littlo

avigad committed 6 years ago

92a5e0b1

feat(*): add various small lemmas

avigad committed 6 years ago

206a7a11

feat(data/list/basic): mem_rotate

ChrisHughes24 committed 6 years ago

4f7853a1

refactor(ring_theory/localization): rename of to mk, and define of (#765)

jcommelin committed 6 years ago

05449a06

feat(ring_theory/ideals): make ideal.quotient.field a discrete_field (#777)

ChrisHughes24 committed 6 years ago

Verified eb033cfe

refactor(algebra/group): generalise and extend the API for with_zero (#762)

jcommelin committed 6 years ago

e6a3ca81

feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764)

jcommelin committed 6 years ago

781d1875

fix(tactic/linarith): typo

robertylewis committed 6 years ago

81f85308

feat(topology/basic): Add instances for subset/inter/union for opens(X) (#763)

jcommelin committed 6 years ago

08d4d17b

refactor(data/subtype): organise in namespaces, use variables, add two simp-lemmas (#760)

jcommelin committed 6 years ago

477338d2

feat(group_theory/quotient_group): map is a group hom (#761)

jcommelin committed 6 years ago

af2cf74a

feat(data/finset) remove unnecessary assumption from card_eq_succ (#772)

kckennylau committed 6 years ago

dfa855c2

fix(doc/tactics): linarith doc is outdated [ci-skip]

robertylewis committed 6 years ago

cfde449a

fix(tactic/linarith): fix bug in strengthening of strict nat/int inequalities

robertylewis committed 6 years ago

6c71ac0b

feat(ring_theory/ideal_operations): ideals form a commutative semiring (#771)

kckennylau committed 6 years ago

4667d2c2

Newer Older