Commits leanprover-community/mathlib

chore(category_theory/closed/cartesian): make exp right-associative (#11172)

dwarn committed 4 years ago

8db2fa05

feat(data/quot): Add quotient pi induction (#11137)

prakol16 committed 4 years ago

559951cd

feat(analysis/normed_space/banach_steinhaus): prove the standard Banach-Steinhaus theorem (#10663)

j-loreaux committed 4 years ago

200f47d3

feat(data/polynomial/ring_division): golf and generalize `leading_coeff_div_by_monic_of_monic` (#11077)

pechersky committed 4 years ago

ea710ca6

feat(data/int/gcd): add theorem `gcd_least_linear` (#10743)

stuart-presnell committed 4 years ago

8ec59f9c

chore(data/sym/basic): golf and add missing simp lemmas (#11160)

eric-wieser committed 4 years ago

e4607f8f

feat(algebra/star/self_adjoint): define the self-adjoint elements of a star additive group (#11135)

dupuisf committed 4 years ago

fbbbdfa0

feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)

pechersky committed 4 years ago

fdf09df0

feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)

ocfnash committed 4 years ago

c4caf0ee

feat(data/list/indexes): map_with_index_eq_of_fn (#11163)

pechersky committed 4 years ago

9a38c196

chore(data/equiv/basic): missing dsimp lemmas (#11159)

eric-wieser committed 4 years ago

b92afc90

feat(category_theory/sites/plus): Adds a functorial version of `J.diagram P`, functorial in `P`. (#11155)

adamtopaz committed 4 years ago

bcf1d2dd

feat(category_theory/limits/functor_category): Some additional isomorphisms involving (co)limits of functors. (#11152)

adamtopaz committed 4 years ago

7b387924

feat(data/list/count): add lemma `count_le_count_map` (#11148)

stuart-presnell committed 4 years ago

b142b697

feat(ring_theory/localization): Transferring `is_localization` along equivs. (#11146)

erdOne committed 4 years ago

dc57b544

feat(data/dfinsupp/order): Pointwise order on finitely supported dependent functions (#11138)

YaelDillies committed 4 years ago

bc5e0081

feat(algebra/homology): Construction of null homotopic chain complex … (#11125)

joelriou committed 4 years ago

2e8ebdc0

feat(combinatorics/configuration): Variant of `exists_injective_of_card_le` (#11116)

tb65536 committed 4 years ago

ff7e837a

refactor(algebra/big_operators/basic): Reorder lemmas (#11113)

tb65536 committed 4 years ago

1fd70b1b

feat(data/fin/tuple): new directory and file on sorting (#11096)

robertylewis committed 4 years ago

99e3ffbd

feat(category_theory/bicategory/basic): define bicategories (#11079)

yuma-mizuno committed 4 years ago

06a01971

feat(data/{fin,multi}set/powerset): add some lemmas about powerset_len (#10866)

alexjbest committed 4 years ago

a5573f37

refactor(algebra/group/hom_instances): relax semiring to non_unital_non_assoc_semiring in add_monoid_hom.mul (#11165)

mans0954 committed 4 years ago

78a9900b

docs(data/sum/basic): Expand module docstring and cleanup (#11158)

YaelDillies committed 4 years ago

dc1525fb

feat(tactic/itauto): add support for [decidable p] assumptions (#10744)

digama0 committed 4 years ago

e1a8b886

feat(category_theory/currying): `flip` is isomorphic to uncurrying, swapping, and currying. (#11151)

adamtopaz committed 4 years ago

7f928329

chore(algebra/ring/comp_typeclasses): fix doctrings (#11150)

dupuisf committed 4 years ago

3dad7c8c

feat(analysis/normed_space/operator_norm): generalize linear_map.bound_of_ball_bound (#11140)

robertylewis committed 4 years ago

682f1e63

feat(data/nat/choose/basic): choose_eq_zero_iff (#11120)

pechersky committed 4 years ago

c0b5ce12

feat(analysis/special_functions/log): add log_div_self_antitone_on (#10985)

BoltonBailey committed 4 years ago

993a470e