leanprover-community/mathlib

Pull Requests Commits

doc(order/succ_pred/basic): fix typo (#12501)

meithecatte committed 4 years ago

65095fe1

feat(algebra/group/to_additive): add to_additive doc string linter (#12487)

nomeata committed 4 years ago

47182da5

chore(set_theory/game/nim): General golfing (#12471)

vihdzp committed 4 years ago

ccdcce13

feat(algebra/homology/homotopy) : `mk_coinductive` (#12457)

jjaassoonn committed 4 years ago

b3fba033

feat(analysis/normed_space): allow non-unital C^* rings (#12327)

kim-em committed 4 years ago

14997d0e

chore(counterexamples/canonically_ordered_comm_semiring_two_mul): golf (#12504)

eric-wieser committed 4 years ago

74746bde

chore(*): move `has_scalar` instances before `add_comm_monoid` instances (#12502)

eric-wieser committed 4 years ago

5f6d30ec

feat(measure_theory/integral/periodic.lean): add lemma `function.periodic.tendsto_at_bot_interval_integral_of_pos'` (#12500)

ocfnash committed 4 years ago

e409a904

feat(ring_theory/coprime/basic): lemmas about multiplying by units (#12480)

Ruben-VandeVelde committed 4 years ago

390554d2

chore(number_theory/number_field): golf `int.not_is_field` (#12451)

Aresh-P committed 4 years ago

9728bd25

feat(algebra/associated): add pow_not_prime (#12493)

Ruben-VandeVelde committed 4 years ago

1b4ee53b

feat(measure_theory/function/uniform_integrable): Uniform integrability and Vitali convergence theorem (#12408)

kex-y committed 4 years ago

f28023e9

feat(probability_theory/stopping): define progressively measurable processes (#11350)

kex-y committed 4 years ago

1ee91a5c

feat(data/real/nnreal): floor_semiring instance (#12495)

eric-wieser committed 4 years ago

e871be25

feat(category_theory): (co)kernels of biproduct projection and inclusion (#12394)

javra committed 4 years ago

8d2ffb8f

docs(overview): Add overview of model theory (#12496)

awainverse committed 4 years ago

85a415e9

fix(tactic/interactive): use non-interactive admit tactic (#12489)

kmill committed 4 years ago

3c3c3bc1

feat(measure_theory/integral/periodic): further properties of periodic integrals (#12488)

ocfnash committed 4 years ago

5f2a6ac6

fix(number_theory/modular): prefer `coe` over `coe_fn` in lemma statements (#12445)

eric-wieser committed 4 years ago

c95ce52d

chore(algebra/order/{group,monoid}): trivial lemma about arithmetic on `with_top` and `with_bot` (#12491)

eric-wieser committed 4 years ago

f451e09a

chore(algebra/order/nonneg): add `nonneg.coe_nat_cast` (#12490)

eric-wieser committed 4 years ago

65ac316c

feat(analysis/normed_space): non-unital normed rings (#12326)

kim-em committed 4 years ago

16b67661

feat(category_theory/limits): limit preservation properties of functor.left_op and similar (#12168)

TwoFX committed 4 years ago

9ed43666

chore(data/equiv/basic): rename `involutive.to_equiv` to `to_perm` (#12486)

urkud committed 4 years ago

900ce6fc

feat(algebra/group/to_additive): let to_additive turn `pow` into `nsmul` (#12477)

nomeata committed 4 years ago

eb46e7e3

refactor(set_theory/*): `o.out.r` → `<` (#12468)

vihdzp committed 4 years ago

d704f27e

feat(analysis/normed/group/hom): add a module instance (#12465)

eric-wieser committed 4 years ago

9dd8ec1e

feat(measure_theory/group/arithmetic): actions by int and nat are measurable (#12464)

eric-wieser committed 4 years ago

0b86bb8d

feat(data/nat/basic): add one_le_div_iff (#12461)

kbuzzard committed 4 years ago

3f353db2

feat(measure_theory/constructions/polish): injective images of Borel sets in Polish spaces are Borel (#12448)

sgouezel committed 4 years ago

2675b5c3

Newer Older