Commits leanprover-community/mathlib3

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

YaelDillies committed 3 years ago

8430aae3

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

YaelDillies committed 3 years ago

08323cda

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

javra committed 3 years ago

3a061790

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

YaelDillies committed 3 years ago

b7cba576

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

YaelDillies committed 3 years ago

b6c96ef7

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

fpvandoorn committed 3 years ago

e49ac91b

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

adomani committed 3 years ago

62b33339

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

kex-y committed 3 years ago

777d1ec1

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

kkytola committed 3 years ago

6490ee3a

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

adomani committed 3 years ago

91cbe460

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

ADedecker committed 3 years ago

8044794f

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

robertylewis committed 3 years ago

79abf670

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

vihdzp committed 3 years ago

e8b581a7

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

fpvandoorn committed 3 years ago

0f9edf98

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

YaelDillies committed 3 years ago

c956647c

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

YaelDillies committed 3 years ago

22c42912

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

eric-wieser committed 3 years ago

e5f82363

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

jjaassoonn committed 3 years ago

0821eef1

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

vihdzp committed 3 years ago

f1091b38

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

astrainfinita committed 3 years ago

c30131fb

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

eric-wieser committed 3 years ago

761801fd

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

nomeata committed 3 years ago

5c2088ed

feat(set_theory/cofinality): Basic fundamental sequences (#13326)

vihdzp committed 3 years ago

7d61199a

feat(special_functions/pow): continuity of real to complex power (#13244)

loefflerd committed 3 years ago

ba455ea6

feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172)

Julian committed 3 years ago

cf3b996e

feat(category_theory/path_category): canonical quotient of a path category (#13159)

kim-em committed 3 years ago

82ef19af

refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)

BoltonBailey committed 3 years ago

82615017

feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)

eric-wieser committed 3 years ago

21bbe900

fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507)

kim-em committed 3 years ago

b87e193d

feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)

riccardobrasca committed 3 years ago

9f22a367