leanprover-community/mathlib

Pull Requests Commits

feat(data/matrix): matrix and vector notation (#2656)

Vierkantor committed 5 years ago

11415339

chore(*): unify use of left and right for injectivity lemmas (#2655)

TwoFX committed 5 years ago

34a0c8c5

chore(topology/instances/ennreal): add +1 version of `tsum_eq_supr_sum` (#2633)

urkud committed 5 years ago

77b3d504

feat(analysis/normed_space): add Mazur-Ulam theorem (#2214)

urkud committed 5 years ago

ff184e6d

feat(number_theory/basic): dvd_sub_pow_of_dvd_sub (#2640)

jcommelin committed 5 years ago

3f216bc6

fix(order/filter/basic): markdown error in module doc (#2664)

robertylewis committed 5 years ago

61b59ec5

feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623)

jcommelin committed 5 years ago

295b87ec

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

leanprover-community-bot committed 5 years ago

f0e78172

feat(data/list): assorted lemmas (#2651)

urkud committed 6 years ago

8c887216

test(tactic/norm_num): import tests from lean core (#2654)

digama0 committed 6 years ago

eb9e3824

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

leanprover-community-bot committed 6 years ago

a87f326d

refactor(data/real/pi): add tactics for pi computation (#2641)

digama0 committed 6 years ago

e777d0b4

feat(algebra/ring): monoid structure on `R →+* R` (#2649)

urkud committed 6 years ago

ff37fb8a

refactor(data/fintype/basic): weaken assumptions of set.fintype (#2650)

digama0 committed 6 years ago

7146082c

feat(*): prove some `*.iterate` theorems (#2647)

urkud committed 6 years ago

b9bdc678

fix(library_search): use custom apply tactic for the main goal, as well as subgoals (#2648)

kim-em committed 6 years ago

8c6b14ea

feat(meta/uchange): universe lifting and lowering in meta (#2627)

gebner committed 6 years ago

3710744b

chore(algebra/char_zero): add `∀ n : ℕ, (n + 1 : α) ≠ 0` (#2644)

urkud committed 6 years ago

b248481b

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

leanprover-community-bot committed 6 years ago

75900904

chore(*): move to lean-3.11.0 (#2632)

jcommelin committed 6 years ago

81f97bdf

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

leanprover-community-bot committed 6 years ago

a584d527

feat(algebra/ordered_*): arithmetic operations on monotone functions (#2634)

urkud committed 6 years ago

9f33b7dd

chore(logic/embedding,order/order_iso): review (#2618)

urkud committed 6 years ago

d04429fa

refactor(computability/turing_machine): add list_blank (#2605)

digama0 committed 6 years ago

08d43163

feat(tactic/norm_num): new all-lean norm_num (#2589)

digama0 committed 6 years ago

b7698468

chore(data/finset): drop `to_set`, use `has_lift` instead (#2629)

urkud committed 6 years ago

20c74188

feat(data/nat/basic): add `mod_add_mod` and `add_mod_mod` (#2635)

shingtaklam1324 committed 6 years ago

e1192f35

feat(data/nat/cast): nat.cast_with_bot (#2636)

digama0 committed 6 years ago

96efc220

feat(src/ring_theory/algebra): define equivalence of algebras (#2625)

Oliver Nash committed 6 years ago

67e19cd9

chore(`analysis/normed_space/banach`): minor review (#2631)

urkud committed 6 years ago

fc8c4b9f

Newer Older