leanprover-community/mathlib

Pull Requests Commits

fix(data/padics): misstated lemma (#1718)

robertylewis committed 6 years ago

5a6a67fc

feat(analysis/normed_space/operator_norm): extension of a uniform continuous function (#1649)

Zhouhang Zhou committed 6 years ago

0744a3a9

feat(algebra/group_power): prove Bernoulli's inequality for `a ≥ -2` (#1709)

urkud committed 6 years ago

d67e527a

feat(algebra/group; data/nat) lemmas for sub sub assoc (#1712)

b-mehta committed 6 years ago

d4fd7227

fix(tactic/ring): bugfix ring sub (#1714)

digama0 committed 6 years ago

db6eab2e

feat(.travis): add linting of new changes to CI (#1634)

robertylewis committed 6 years ago

740168bf

chore(scripts/nolint): regenerate nolints

Rob Lewis committed 6 years ago

02659d63

fix(tactic/omega): use eval_expr' (#1711)

digama0 committed 6 years ago

8d7f093b

lemmas about powers of elements (#1688)

jlpaca committed 6 years ago

e3be70db

feat(algebra/order): define `forall_lt_iff_le` and `forall_lt_iff_le'` (#1707)

urkud committed 6 years ago

b0520a31

feat(data/set/intervals): more lemmas (#1665)

urkud committed 6 years ago

5d5da7e6

feat(data/option): add `some_ne_none`, `bex_ne_none`, `ball_ne_none` (#1708)

urkud committed 6 years ago

895f1ae0

feat(data/real/nnreal): define `nnreal.gi : galois_insertion of_real coe` (#1699)

urkud committed 6 years ago

6b408eb1

feat(data/nat/enat): add_right_cancel and other (#1705)

ChrisHughes24 committed 6 years ago

af43a2bc

feat(algebra/order_functions): define `min/max_mul_of_nonneg` (#1698)

urkud committed 6 years ago

0d94020c

chore(data/set): use `Sort*` in more lemmas (#1706)

urkud committed 6 years ago

3f9c4d88

feat(group_theory/congruence): create file about congruence relations (#1690)

101damnations committed 6 years ago

428aec90

feat(data/finset): new union, set difference, singleton lemmas (#1702)

b-mehta committed 6 years ago

0a794fac

chore(data/set/lattice): get most proofs from `pi` instance. (#1685)

urkud committed 6 years ago

fafdcfdc

feat(analysis/normed_space/finite_dimension): finite-dimensional spaces on complete fields (#1687)

sgouezel committed 6 years ago

d19f7bc6

chore(algebra/order_functions): rename `min/max_distrib_of_monotone` (#1697)

urkud committed 6 years ago

7c5f282d

feat(algebra/big_operators): sum_Ico_succ_top and others (#1692)

ChrisHughes24 committed 6 years ago

9607bbf8

chore(order_functions): use weakly implicit brackets in strict mono (#1701)

ChrisHughes24 committed 6 years ago

f5385fe0

fix(topology/dense_embeddings): tweaks (#1684)

PatrickMassot committed 6 years ago

474004f1

refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit (#1691)

urkud committed 6 years ago

1805f16a

feat(data/int/parity): not_even_iff (#1694)

ChrisHughes24 committed 6 years ago

10343579

feat(algebra/pointwise): set.add_comm_monoid (#1696)

kbuzzard committed 6 years ago

e863c088

Add lemma for injective pow (#1683)

b-mehta committed 6 years ago

6b1ab646

feat(data/nat/modeq): add_div and others (#1689)

ChrisHughes24 committed 6 years ago

6ebb7e78

doc(order/bounds,order/conditionaly_complete_lattice): add some docs (#1686)

urkud committed 6 years ago

40de4fcb

Newer Older