Commits leanprover-community/mathlib

Merge remote-tracking branch 'origin/master' into delete_deprecated

kim-em committed 3 years ago

fa0906dc

chore(ring_theory/hahn_series, topology/locally_constant/algebra): add missing `non_unital_non_assoc_ring` instances (#13504)

j-loreaux committed 3 years ago

37d02d3d

chore(algebra/ring/{pi, prod}): fix errors in `ring_hom` for `pi` and `prod`. (#13501)

j-loreaux committed 3 years ago

3c20253b

chore(analysis/normed_space/finite_dimension): golf a proof (#13491)

eric-wieser committed 3 years ago

b54591f7

chore(data/nat/factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473)

stuart-presnell committed 3 years ago

fd08afe3

feat(order/bounded_order): Strictly monotone functions preserve maximality (#13434)

YaelDillies committed 3 years ago

d89160b5

feat(data/real/ennreal): Order properties of addition (#13371)

YaelDillies committed 3 years ago

5c75390e

feat(order/upper_lower): Principal upper/lower sets (#13069)

YaelDillies committed 3 years ago

546618eb

feat(set_theory/cardinal): `lt_omega_of_fintype` (#13365)

vihdzp committed 3 years ago

d790b4b8

feat(number_theory/legendre_symbol/quadratic_reciprocity): replace `[fact (p % 2 = 1)]` arguments by `(p ≠ 2)` (#13474)

MichaelStollBayreuth committed 3 years ago

e18ea79e

feat(computability/partrec_code): add eval prec helpers (#11945)

BoltonBailey committed 3 years ago

82348a60

chore(scripts): update nolints.txt (#13493)

leanprover-community-bot committed 3 years ago

279b7f34

feat(analysis/convex): golf some proofs (#13451)

urkud committed 3 years ago

e6322c6a

feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)

eric-wieser committed 3 years ago

b90e770f

chore(algebra/big_operators/fin): moving lemmas (#13331)

joelriou committed 3 years ago

9380977b

feat(topology/[separation, homeomorph]): separation properties are topological invariants (#13401)

ADedecker committed 3 years ago

7c7f3514

feat(topology/algebra/order): extreme value thm for a function continuous on a closed set (#13348)

urkud committed 3 years ago

49e41eb5

chore(scripts): update nolints.txt (#13482)

leanprover-community-bot committed 3 years ago

f4f46cd5

feat(data/finsupp/basic): add a few lemmas, mostly about `finsupp.filter` (#13457)

urkud committed 3 years ago

d4fda045

chore(number_theory/*): Weaken assumptions (#13443)

YaelDillies committed 3 years ago

96667b51

chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419)

YaelDillies committed 3 years ago

018e9b57

chore(logic/encodable/basic): Rename `encodable` instances (#13396)

YaelDillies committed 3 years ago

8decd4b1

feat(algebra/order/monoid): Co/contravariant classes for `with_bot`/`with_top` (#13369)

YaelDillies committed 3 years ago

91a43e71

feat(data/polynomial/eval): generalize smul lemmas (#13479)

astrainfinita committed 3 years ago

874dde52

feat(data/polynomial/taylor): add `taylor_alg_hom` (#13477)

astrainfinita committed 3 years ago

010f09e7

feat(data/polynomial/eval): add `protected` on some lemmas about `polynomial.map` (#13478)

astrainfinita committed 3 years ago

f7430cd7

feat(topology/stone_cech): add stone_cech_hom_ext (#13472)

mapehe committed 3 years ago

862a5854

feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182)

mlavrent committed 3 years ago

449e06a9

chore(number_theory/function_field): fix typo (#13464)

mariainesdff committed 3 years ago

c988c622

refactor(number_theory/legendre_symbol/): move Gauss/Eisenstein lemma code to separate file (#13449)

MichaelStollBayreuth committed 3 years ago

fbff76b5