leanprover-community/mathlib3

Pull Requests Commits

feat(order/grade): Graded orders (#11308)

YaelDillies committed 4 years ago

e728cfd4

feat(number_theory/modular): fundamental domain part 2 (#8985)

AlexKontorovich committed 4 years ago

8110ab9d

chore(algebra/algebra/spectrum): lemmas about the zero ring (#13568)

eric-wieser committed 4 years ago

ba556a70

ci(gitpod): update leanproject version (#13567)

eric-wieser committed 4 years ago

81453334

chore(set_theory/ordinal/basic): Small style tweaks (#13561)

vihdzp committed 4 years ago

aeef727f

refactor(group_theory/{submonoid, subsemigroup}/basic): move `mul_mem_class` (#13559)

j-loreaux committed 4 years ago

efab188a

feat(data/nat/pow): add theorem `nat.pow_mod` (#13551)

slerpyyy committed 4 years ago

afe14217

feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538)

fpvandoorn committed 4 years ago

090e59d0

feat(algebra/group_power/lemmas): More lemmas through `to_additive` (#13537)

YaelDillies committed 4 years ago

8430aae3

feat(data/real/ennreal): `tsub` lemmas (#13525)

YaelDillies committed 4 years ago

08323cda

refactor(category_theory): reverse simp lemmas about (co)forks (#13519)

javra committed 4 years ago

3a061790

chore(set_theory/game/*): Protect ambiguous lemmas (#13557)

YaelDillies committed 4 years ago

b7cba576

feat(combinatorics/simple_graph/clique): Clique-free graphs (#13552)

YaelDillies committed 4 years ago

b6c96ef7

feat(analysis/calculus/cont_diff): add more prod lemmas (#13521)

fpvandoorn committed 4 years ago

e49ac91b

chore(algebra/star/chsh): `repeat`ed golf (#13499)

adomani committed 4 years ago

62b33339

feat(measure_theory/measure/measure_space): add some lemmas for the counting measure (#13485)

kex-y committed 4 years ago

777d1ec1

feat(topology/instances/ennreal): Add lemmas about continuity of ennreal subtraction. (#13448)

kkytola committed 4 years ago

6490ee3a

feat(algebra/monoid_algebra/basic): lifts of (add_)monoid_algebras (#13382)

adomani committed 4 years ago

91cbe460

feat(topology/algebra/module/basic): continuous linear maps are automatically uniformly continuous (#13276)

ADedecker committed 4 years ago

8044794f

fix(tactic/apply_rules): separate single rules and attribute names in syntax (#13227)

robertylewis committed 4 years ago

79abf670

feat(order/countable_dense_linear_order): Relax conditions of `embedding_from_countable_to_dense` (#12928)

vihdzp committed 4 years ago

e8b581a7

feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422)

fpvandoorn committed 4 years ago

0f9edf98

feat(order/basic): Simple shortcut lemmas (#13421)

YaelDillies committed 4 years ago

c956647c

chore(number_theory/dioph): Cleanup (#13403)

YaelDillies committed 4 years ago

22c42912

feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)

eric-wieser committed 4 years ago

e5f82363

feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398)

jjaassoonn committed 4 years ago

0821eef1

feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)

vihdzp committed 4 years ago

f1091b38

feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)

astrainfinita committed 4 years ago

c30131fb

feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)

eric-wieser committed 4 years ago

761801fd

feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)

nomeata committed 4 years ago

5c2088ed

Newer Older