leanprover-community/mathlib3

Pull Requests Commits

feat(tactic/squeeze_*): add `squeeze_dsimp` (#3386)

cipher1024 committed 6 years ago

819bd86b

chore(data/polynomial): reduce imports (#3419)

kim-em committed 6 years ago

9d74f9b0

feat (order/order_iso): lemmas about order_isos on lattices (#3397)

awainverse committed 6 years ago

f1b687cd

chore(data/polynomial): break up behemoth file (#3407)

jalex-stark committed 6 years ago

33d45bf0

feat(meta/expr): add tactic_format instance for declaration (#3390)

robertylewis committed 6 years ago

6fd4f8fa

feat(data/nat/digits): add lemmas about digits (#3406)

shingtaklam1324 committed 6 years ago

25be04ae

chore(topology/algebra/ordered): rename `lim*_eq_of_tendsto` to `tendsto.lim*_eq` (#3415)

urkud committed 6 years ago

a8c10e1c

feat(tactic/obviously): improve error reporting (#3412)

kim-em committed 6 years ago

1311eb2b

chore(data/opposite): pp_nodot on op and unop (#3413)

kim-em committed 6 years ago

9ca3ce6e

chore(order/directed): use implicit args in `iff`s (#3411)

urkud committed 6 years ago

c1a5ae94

feat(measure_theory): preliminaries for Haar measure (#3195)

fpvandoorn committed 6 years ago

5fe67b77

feat(algebra/ordered_group): instances for additive/multiplicative (#3405)

ChrisHughes24 committed 6 years ago

5f5d6417

refactor(topology/algebra/infinite_sum): review (#3371)

urkud committed 6 years ago

a41a3074

feat(logic/basic) forall_imp (#3391)

kmill committed 6 years ago

503a40aa

feat(category_theory/pullback): make the is_limit helper lemmas more ergonomic (#3398)

kim-em committed 6 years ago

51a75ffe

feat(geometry/manifold/times_cont_mdiff): smooth functions between manifolds (#3387)

sgouezel committed 6 years ago

8495f76b

chore(data/set/basic): simp attribute on set.image_subset_iff (#3394)

jalex-stark committed 6 years ago

708e4813

chore(category_theory/natural_isomorphism): move lemmas to correct namespace, add simp lemma (#3401)

kim-em committed 6 years ago

6c1ae3b1

feat(algebra/polynomial): big_operators lemmas for polynomials (#3378)

jalex-stark committed 6 years ago

f7825bf5

feat(data/qpf): uniformity iff preservation of supp (#3388)

cipher1024 committed 6 years ago

bcf61df2

refactor(category_theory/finite_limits): missing piece of #3320 (#3400)

kim-em committed 6 years ago

02f2f947

chore(category_theory/limits/over): split a slow file (#3399)

kim-em committed 6 years ago

a0846da1

feat(analysis/normed_space): complex Hahn-Banach theorem (#3286)

Ruben-VandeVelde committed 6 years ago

0fff477d

feat(category_theory/kernels): kernel_iso_of_eq (#3372)

kim-em committed 6 years ago

5f01b544

chore(*): generalize tensor product to semirings (#3389)

kckennylau committed 6 years ago

58dde5b8

add notes about things to do

kim-em committed 6 years ago

c059aafe

chore(linear_algebra/nonsingular_inverse): swap update_row/column names (#3393)

pechersky committed 6 years ago

04109461

feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces (#3377)

jsm28 committed 6 years ago

32c75d01

feat(ring_theory/ideal_over): lemmas for nonzero ideals lying over nonzero ideals (#3385)

Vierkantor committed 6 years ago

11322372

feat(analysis/normed_space/real_inner_product): orthogonal subspaces (#3369)

jsm28 committed 6 years ago

45477c8f

Newer Older