Commits leanprover-community/mathlib

Merge remote-tracking branch 'origin/FR_order_refactor14' into FR_order_refactor12

astrainfinita committed 3 years ago

02266b49

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

f1f72ab9

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

472fda06

Merge remote-tracking branch 'origin/FR_order_refactor13' into FR_order_refactor12

astrainfinita committed 3 years ago

c9eef970

feat(algebra/order/monoid_lemmas_zero_lt): generalize lemmas

astrainfinita committed 3 years ago

0613b872

Merge remote-tracking branch 'origin/FR_order_refactor11' into FR_order_refactor14

astrainfinita committed 3 years ago

e62e6423

chore(algebra/order/monoid_lemmas_zero_lt): create aliases for `left` lemmas

astrainfinita committed 3 years ago

3c9aa73c

chore(algebra/order/monoid_lemmas_zero_lt): move all positivity assumptions to the first place

astrainfinita committed 3 years ago

562d54fe

feat(group_theory/group_action/defs): `additive`/`multiplicative` instances (#15719)

YaelDillies committed 3 years ago

4e76ad05

feat(data/nat/factorization/basic): define `ord_proj[p]` and `ord_compl[p]`, prove basic lemmas (#15589)

stuart-presnell committed 3 years ago

6c135283

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