leanprover-community/mathlib

Pull Requests Commits

kim-em committed 2 years ago

da0111c4

feat(ring_theory/tensor_product): add missing scalar tower instances (#19143)

eric-wieser committed 2 years ago

88fcdc3d

feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875)

eric-wieser committed 2 years ago

8047de4d

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

leanprover-community-bot committed 2 years ago

573eea92

chore(set_theory/ordinal/basic): golf (#18547)

astrainfinita committed 2 years ago

8ea5598d

feat(order/irreducible): Sup-irreducible elements (#18999)

YaelDillies committed 2 years ago

bf2428c9

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

leanprover-community-bot committed 2 years ago

08b081ea

fix: handle archive and counterexamples correctly when adding port comments (#19237)

eric-wieser committed 2 years ago

88e6ad41

fix(tactic/linarith): instantiate metavariables in linarith (#19233)

eric-wieser committed 2 years ago

016138c2

feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

vihdzp committed 2 years ago

31b269b6

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

Older