Commits leanprover-community/mathlib

fix(category_theory/elements): speed up `groupoid_of_elements` (#13372)

alreadydone committed 4 years ago

fdd68d9b

chore(algebra/module/basic): generalize to add_monoid_hom_class (#13346)

eric-wieser committed 4 years ago

bf1b813e

feat(data/list/basic): add a theorem about last and append (#13336)

sorawee committed 4 years ago

955cb8e6

feat(algebra/order/monoid_lemmas_zero_lt): add lemmas assuming `mul_zero_class` `preorder` (#13297)

astrainfinita committed 4 years ago

10a3faa4

feat(data/polynomial/algebra_map): remove some lemmas about `aeval`, add `protected` on `polynomial.map_list_prod` (#13294)

astrainfinita committed 4 years ago

fe1c78af

feat(analysis/convex/strict_convex_space): Ray characterization of `∥x - y∥` (#13293)

YaelDillies committed 4 years ago

483b7df9

feat(topology/uniform_space/uniform_convergence_topology): define the uniform structure of uniform convergence (#13073)

ADedecker committed 4 years ago

f1c98ba8

feat(order/basic): More order instances for `subtype` (#13134)

YaelDillies committed 4 years ago

7ba9c3fe

feat(algebraic_geometry/projective_spectrum): structure sheaf of Proj of graded ring (#13072)

jjaassoonn committed 4 years ago

0453d606

feat(analysis/normed/normed_field): Pi types form a normed ring (#12912)

eric-wieser committed 4 years ago

f94cd0f1

feat(data/fin/tuple/nat_antidiagonal): add an equiv and some TODO comments. (#13338)

eric-wieser committed 4 years ago

887f9338

chore(representation_theory/invariants): clean up some simps (#13337)

Ruben-VandeVelde committed 4 years ago

455bc657

feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327)

kim-em committed 4 years ago

e8339bd6

chore(*): remove numerous edge cases from lemmas (#13316)

alexjbest committed 4 years ago

4a070542

feat(number_theory/quadratic_reciprocity): change order of arguments … (#13311)

MichaelStollBayreuth committed 4 years ago

a839f4dc

feat(probability/integration): characterize indep_fun by expected product of comp (#13270)

vbeffara committed 4 years ago

4e1102a0

feat(data/set/basic): Missing `set.image_perm` (#13242)

MantasBaksys committed 4 years ago

a521a32e

feat(computability/*): Automata lemmas (#13194)

YaelDillies committed 4 years ago

dee49588

feat(number_theory/cyclotomic/primitive_roots): add `pow_sub_one_norm_prime_pow_ne_two` (#13152)

riccardobrasca committed 4 years ago

77ae0912

feat(measure_theory/measure/haar): Add the Steinhaus Theorem (#12932)

MantasBaksys committed 4 years ago

04250c8d

feat(data/sign): the sign function (#12835)

ericrbg committed 4 years ago

cea5e4bb

feat(combinatorics/simple_graph/connectivity): induced maps on walks and paths (#13310)

kmill committed 4 years ago

695a2b69

chore(category_theory/*): reduce imports (#13305)

kim-em committed 4 years ago

a447dae9

feat(combinatorics/simple_graph/{connectivity,adj_matrix}): powers of adjacency matrix (#13304)

kmill committed 4 years ago

5e8d6bb3

chore(category_theory): switch ulift and filtered in import hierarchy (#13302)

kim-em committed 4 years ago

bfd53845

feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense (#12955)

kex-y committed 4 years ago

dcb6c865

feat(ring_theory/coprime/lemmas): alternative characterisations of pairwise coprimeness (#12911)

pbazin committed 4 years ago

797c7133

feat(data/option/basic): add `option.coe_get` (#13081)

stuart-presnell committed 4 years ago

67d60972

refactor(category_theory/differential_object): simp only -> simp_rw (#13333)

kim-em committed 4 years ago

41398242

chore(category_theory/monoidal/discrete): typo in to_additive name (#13332)

kim-em committed 4 years ago

c7e76bc8