leanprover-community/mathlib

Pull Requests Commits

feat({data/{finset,set},order/filter}/pointwise): More basic API (#13899)

YaelDillies committed 3 years ago

4dfbcac3

ci(gitpod): do not rerun get-cache if a workspace is reloaded (#13949)

eric-wieser committed 3 years ago

f8206717

chore(algebra/group/units): add a lemma about is_unit on a coerced unit (#13947)

eric-wieser committed 3 years ago

69701295

chore(linear_algebra/free_module): fix name in doc (#13942)

alexjbest committed 3 years ago

bd944fe1

chore(data/matrix/basic): add more lemmas about `conj_transpose` and `smul` (#13938)

eric-wieser committed 3 years ago

4f7603c7

feat(analysis/normed/normed_field): limit of `∥a * x∥` as `∥x∥ → ∞` (#13819)

urkud committed 3 years ago

7eacca31

Update CODE_OF_CONDUCT.md (#13965)

madvorak committed 3 years ago

03fbe7de

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

leanprover-community-bot committed 3 years ago

63875eae

feat(tactic/alias): fix alias docstrings for implications from iffs (#13944)

alexjbest committed 3 years ago

116435d6

feat(representation_theory): Action V G is rigid whenever V is (#13738)

kim-em committed 3 years ago

524793de

feat(data/sum/basic): Shortcuts for the ternary sum of types (#13678)

YaelDillies committed 3 years ago

b1da074a

feat(algebra/group/{pi, opposite}): add missing pi and opposite defs for `mul_hom` (#13956)

j-loreaux committed 3 years ago

0c9b7263

feat(data/matrix/block): add `matrix.block_diag` and `matrix.block_diag'` (#13918)

eric-wieser committed 3 years ago

50781196

feat(analysis/special_functions/log/monotone): add lemmas (#13848)

BoltonBailey committed 3 years ago

50fd3d6a

docs(algebra/ring/opposite): fix docstring for `ring_hom.from_opposite` (#13957)

j-loreaux committed 3 years ago

1e189356

feat(representation_theory/Action): lemma about isomorphisms in `Action G V` (#13951)

antoinelab01 committed 3 years ago

36509369

feat(analysis/convex/integral): drop an assumption, add a version (#13920)

urkud committed 3 years ago

9b245e23

refactor(order/filter/pointwise): Localize instances (#13898)

YaelDillies committed 3 years ago

f8c303ea

feat(group_theory/order_of_element): The index-th power lands in the subgroup (#13890)

tb65536 committed 3 years ago

627f81b4

feat(data/list/big_operators): add `list.sublist.prod_le_prod'` etc (#13879)

urkud committed 3 years ago

5696275a

feat(linear_algebra/dual): dual of a finite free module is finite free (#13896)

antoinelab01 committed 3 years ago

9503f733

refactor(set_theory/game/ordinal): Improve API (#13878)

vihdzp committed 3 years ago

eb1a566f

feat(set_theory/game/nim): Add basic API (#13857)

vihdzp committed 3 years ago

28568bdb

feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853)

kim-em committed 3 years ago

a80e5683

feat(set_theory/game/nim): `nim 0` is a relabelling of `0` and `nim 1` is a relabelling of `star` (#13846)

vihdzp committed 3 years ago

edf6cefa

feat(algebra/ring/idempotents): Introduce idempotents (#13830)

mans0954 committed 3 years ago

fd8474f5

feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu theorem (#9862)

kkytola committed 3 years ago

91c0ef86

ci(workflows/dependent-issues): run once every 15 mins, instead of on every merged PR (#13940)

jcommelin committed 3 years ago

90d6f271

chore(analysis/analytic_composition): weaken some typeclass arguments (#13924)

eric-wieser committed 3 years ago

aabcd895

feat(set_theory/game/{pgame, basic}): Add more order lemmas (#13807)

vihdzp committed 3 years ago

209bb5d4

Newer Older