leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into acl-Wielandt

Antoine Chambert-Loir committed 2 years ago

ff084eeb

Antoine Chambert-Loir committed 2 years ago

8e962b1e

chore(*): add mathlib4 synchronization comments (#19231)

leanprover-community-bot committed 2 years ago

2fe465de

fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981)

eric-wieser committed 2 years ago

c1acdccd

feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738)

eric-wieser committed 2 years ago

6b711d2b

feat(data/*/interval): `finset.uIcc` on concrete structures (#18838)

YaelDillies committed 2 years ago

1d29de43

feat(order/well_founded_set): `prod.lex` is well-founded (#18665)

YaelDillies committed 2 years ago

2c84c2c5

feat(group_theory/order_of_element): Order in `α × β` (#18719)

YaelDillies committed 2 years ago

d07245fd

feat(analysis/calculus/fderiv/mul): derivative of inverse in division rings (#19127)

eric-wieser committed 2 years ago

d608fc5d

feat(*/prod): `prod_prod_prod` equivs (#19235)

eric-wieser committed 2 years ago

cd391184

feat(analysis/inner_product_space/of_norm): Create an inner product from a norm (#4798)

hrmacbeth committed 2 years ago

baa88307

fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument (#19228)

Komyyy committed 2 years ago

b01d6eb9

feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103)

eric-wieser committed 2 years ago

41bef4ae

fix(tactic/interval_cases): instantiate metavars (#19232)

eric-wieser committed 2 years ago

d3b54a9f

feat(data/list/dedup): Lemmas about `list.dedup` (#19142)

dtumad committed 2 years ago

d9e96a3e

feat(analysis/convex): convexity of n-ary sums (#18943)

eric-wieser committed 2 years ago

92bd7b1f

feat(data/fin/basic): extra instances that cover `fin 0` (#18970)

eric-wieser committed 2 years ago

3a2b5524

feat(data/set/intervals/proj_Icc): Extending from `Ici a` (#18795)

YaelDillies committed 2 years ago

4e24c4bf

feat(data/nat/order/basic): `a + b - 1 ≤ a * b` (#18737)

YaelDillies committed 2 years ago

3ed3f98a

feat(group_theory/sylow): add inverse to card_eq_multiplicity (#18300)

b-reinke committed 2 years ago

bd365b1a

chore(*): add mathlib4 synchronization comments (#19229)

leanprover-community-bot committed 2 years ago

1a51edf1

feat(topology/algebra/module/strong_topology): golf `arrow_congrSL` introduced in #19107 (#19128)

ADedecker committed 2 years ago

8905e5ed

chore(topology/sheaves): revert universe generalizations from #19153 (#19230)

kim-em committed 2 years ago

5dc6092d

chore(*): add mathlib4 synchronization comments (#19226)

leanprover-community-bot committed 2 years ago

728ef9db

refactor: redefine `bundle.total_space` (#19221)

urkud committed 2 years ago

e473c319

feat(linear_algebra/matrix/schur_complement): invertibility of block matrices (#19156)

eric-wieser committed 2 years ago

a176cb12

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

leanprover-community-bot committed 2 years ago

44b3f423

chore(*): add mathlib4 synchronization comments (#19220)

leanprover-community-bot committed 2 years ago

d0b19368

refactor(*): move all `mk_simp_attribute` commands to 1 file (#19223)

urkud committed 2 years ago

48fb5b52

chore(category_theory/concrete_category): reorder universes (#19222)

kim-em committed 2 years ago

311ef8c4

Older