Commits leanprover-community/mathlib3

fix(tactic/core): fix unpopulated format string

eric-wieser committed 3 years ago

374e5d99

feat(data/list/forall2): add `list.forall₂_iff_nth_le` (#16073)

madvorak committed 3 years ago

bb289539

feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism. (#15711)

erdOne committed 3 years ago

e83ba8f5

feat(data/polynomial): Polynomial modules (#15065)

erdOne committed 3 years ago

b6041198

refactor(order/rel_classes): redefine `is_well_order` in terms of `is_well_founded` (#15729)

vihdzp committed 3 years ago

08931580

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

leanprover-community-bot committed 3 years ago

f5de6ed7

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial` (#15889)

alreadydone committed 3 years ago

e14ff257

feat(algebra/order/ring): add some instances about covariance (#14763)

astrainfinita committed 3 years ago

64e20fb0

chore(combinatorics/simple_graph): review inhabited instances (#15770)

kmill committed 3 years ago

2303b3e2

feat(algebra/module/localized_module): add characteristic predicate for `localized_module` (#15507)

jjaassoonn committed 3 years ago

ea1dd3d3

feat(probability/martingale/convergence): L¹ martingale convergence theorem and Lévy's upwards theorem (#16042)

kex-y committed 3 years ago

d96e92d7

feat(number_theory/legendre_symbol/add_character): change `coe_to_fun` for `add_char` so it includes `of_add` (#16016)

MichaelStollBayreuth committed 3 years ago

01f1f1bc

feat(analysis/locally_convex): Add construction of continuous linear maps (#15922)

mcdoll committed 3 years ago

ce3997c6

feat(linear_algebra/projective_space/subspace): adds lemmas about the span operation and supremums of collections of subspaces (#15596)

Michael14071407 committed 3 years ago

c62c909c

refactor(data/finset/fin): Delete `finset.fin_range` (#15538)

YaelDillies committed 3 years ago

2ccfe543

feat(ring_theory/algebraic): add transcendental.pow (#16057)

Ruben-VandeVelde committed 3 years ago

774c38f0

feat(analysis/special_functions/trigonometric/angle): more on angles equal or not equal to 0 or π (#16055)

jsm28 committed 3 years ago

98a9eb25

feat(order/directed): a subset stable by supremum is `directed_on (≤)` (#16054)

ADedecker committed 3 years ago

0173319e

feat(data/set/basic): Add natural missing lemmas to `set.subsingleton` and slightly refactor (#15886)

linesthatinterlace committed 3 years ago

d9992ade

feat(data/set/basic): Add `set.nontrivial` predicate and API (#15867)

linesthatinterlace committed 3 years ago

1d7f4798

feat(algebra/order/monoid_lemmas_zero_lt): remove primes, add missing lemmas (#14774)

astrainfinita committed 3 years ago

c239c99e

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

leanprover-community-bot committed 3 years ago

7b94ffe4

fix(algebra/category/Group/equivalence_Group_AddGroup): fix typo (#16067)

jjaassoonn committed 3 years ago

d928d9b4

feat(analysis/normed/group/basic): construct a normed group from a seminormed group satisfying `∥x∥ = 0 → x = 0` (#16066)

ADedecker committed 3 years ago

c553a824

chore(*): restore `subsingleton` instances and remove hacks (#16046)

alreadydone committed 3 years ago

b95b8c7a

feat(polynomial/field_division): Add `root_set_prod` and clean up lemma statements (#16035)

tb65536 committed 3 years ago

791852eb

feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min' (#15978)

adomani committed 3 years ago

0398787b

lint(scripts/lint-style): style linter for _inst_ occurences (#15977)

jcommelin committed 3 years ago

0a58aefa

refactor(order/game_add): move `game_add` to its own file (#15885)

vihdzp committed 3 years ago

b7f327b8

refactor(information_theory/hamming): Separate Hamming norm and dist definitions. (#15820)

linesthatinterlace committed 3 years ago

1b42ac37