leanprover-community/mathlib3

Pull Requests Commits

trying the easy version first

dupuisf committed 4 years ago

2e53eb17

dupuisf committed 4 years ago

9a93d709

added matrix.lean

dupuisf committed 4 years ago

2ecb2e08

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

feat(data/polynomial/degree/definition): nat_degree_monomial in ite form (#11123)

pechersky committed 4 years ago

ac976755

feat(data/finset/fold): fold_const, fold_ite (#11122)

pechersky committed 4 years ago

424773a7

feat(order/galois_connection): gc magic (#11114)

PatrickMassot committed 4 years ago

c8a57623

refactor(analysis/normed_space/operator_norm): split a proof (#11112)

urkud committed 4 years ago

f6d0f8d1

feat(data/fin/interval): add lemmas (#11102)

riccardobrasca committed 4 years ago

11de8674

feat(topology/homeomorph): homeo of continuous equivalence from compact to T2 (#11072)

kmill committed 4 years ago

3398efa6

chore(category_theory/adjunction/limits): generalize universe (#11070)

alreadydone committed 4 years ago

7b1c7751

feat(topology/homotopy): Add homotopy product (#10946)

prakol16 committed 4 years ago

d49ae127

feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic_mul (#11005)

riccardobrasca committed 4 years ago

52841fbf

chore(topology/algebra/weak_dual_topology): review (#11141)

urkud committed 4 years ago

655c2f06

feat(analysis/inner_product_space/adjoint): define the adjoint for linear maps between finite-dimensional spaces (#11119)

dupuisf committed 4 years ago

04071ae3

feat(data/nat/prime): min fac of a power (#11115)

b-mehta committed 4 years ago

9443a7b3

feat(logic/small): The image of a small set is small (#11108)

vihdzp committed 4 years ago

0b6f9ebb

feat(combinatorics/simple_graph): lemmas describing edge set of subgraphs (#11087)

b-mehta committed 4 years ago

864a43bc

chore(data/nat/prime): move some results (#11066)

Ruben-VandeVelde committed 4 years ago

8f873b72

feat(analysis/special_functions/log): sum of logs is log of product (#11106)

b-mehta committed 4 years ago

0c149c90

chore(measure_theory/function/lp_space): move `fact`s (#11107)

hrmacbeth committed 4 years ago

23fdf99d

feat(topology/algebra): range of `coe_fn : (M₁ →ₛₗ[σ] M₂) → (M₁ → M₂)` is closed (#11105)

urkud committed 4 years ago

4f3e99a6

feat(analysis/normed_space/dual): add lemmas, golf (#11132)

urkud committed 4 years ago

ea95523d

feat(topology/metric_space/lipschitz): image of a bdd set (#11134)

urkud committed 4 years ago

be17b92a

chore(analysis/normed_space/basic): add `normed_space.unbounded_univ` (#11131)

urkud committed 4 years ago

5bfd9245

split(data/finsupp/multiset): Split off `data.finsupp.basic` (#11110)

YaelDillies committed 4 years ago

5ac87153

Older