leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into eric-wieser/nnnorm-smul

eric-wieser committed 2 years ago

ddaea51a

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

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

leanprover-community-bot committed 2 years ago

9240e8be

feat(analysis/convex/cone/proper): add hyperplane_separation and comap (#19008)

apurvnakade committed 2 years ago

147b2943

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

leanprover-community-bot committed 2 years ago

08b63ab5

chore(category_theory/limits/construction/over): rename default to basic (#19217)

kim-em committed 2 years ago

15db1b4f

feat(analysis/inner_product_space): the adjoint for unbounded operators (#18820)

mcdoll committed 2 years ago

8b981918

feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198)

AntoineChambert-Loir committed 2 years ago

3ff3f2d6

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

leanprover-community-bot committed 2 years ago

30faa0c3

Older