Commits leanprover-community/mathlib

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

feat(algebra/order/with_zero): Add eq_one_of_mul_eq_one lemmas (#15644)

Multramate committed 3 years ago

0d43cc6d

feat(data/list/basic): add `list.length_filter_le` and `list.length_filter_map_le` (#15369)

madvorak committed 3 years ago

d13cc099

feat(topology/algebra/uniform_ring): ring completions and algebra structures (#14841)

mariainesdff committed 3 years ago

0f4d823c

feat(analysis/calculus/cont_diff): `iterated_fderiv[_within]` is linear in the function (#15902)

ADedecker committed 3 years ago

90dc6175

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint (#15859)

TwoFX committed 3 years ago

18302a46

chore(tactic/group): do not swallow errors from simp_core (#15835)

eric-wieser committed 3 years ago

ecb66ca5

feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field (#15795)

tb65536 committed 3 years ago

fae3ce12

refactor(topology/algebra/infinite_sum): generalize `tsum_zero` (#15786)

pechersky committed 3 years ago

adb6142d

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID (#15758)

Paul-Lez committed 3 years ago

0672fa47