Commits leanprover-community/mathlib

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

chore(algebra/group/type_tags): missing simp lemmas (#13553)

eric-wieser committed 3 years ago

16ecb3d1

feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427)

b-mehta committed 3 years ago

839f5086

refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)

j-loreaux committed 3 years ago

6012c219

chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533)

vihdzp committed 3 years ago

e0f78ab3

feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)

j-loreaux committed 3 years ago

2f1a4aff

chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)

YaelDillies committed 3 years ago

c93b99fa

feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)

j-loreaux committed 3 years ago

b2518bee

refactor(analysis/calculus/cont_diff): reorder the file (#13468)

fpvandoorn committed 3 years ago

81c8f310

move(set_theory/*): Organize in folders (#13530)

YaelDillies committed 3 years ago

b86b9272

chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)

Ruben-VandeVelde committed 3 years ago

741d2851

feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)

vihdzp committed 3 years ago

9d6d8c26

feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546)

YaelDillies committed 3 years ago

27a8328b