leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/affine_space/affine_equiv): lemmas about coercion to `affine_map` (#16284)

jsm28 committed 3 years ago

39d5a98c

feat(data/rat/cast): generalize `ext` lemmas (#16268)

urkud committed 3 years ago

3e2fb4c7

refactor(algebra/order/with_zero): Generalize lemmas (#16240)

YaelDillies committed 3 years ago

31297bda

feat(ring_theory/polynomial/basic): generalize `is_domain` to `no_zero_divisors` (#16226)

eric-wieser committed 3 years ago

301a6253

feat(counterexamples/map_floor): `floor`/`ceil` are not preserved under order ring homs (#16198)

YaelDillies committed 3 years ago

9c0a5431

feat(topology/algebra/polynomial): add coeff_le_of_roots_le (#15275)

xroblot committed 3 years ago

ae93ce85

feat(category_theory/preadditive): projective iff variants of Yoneda preserve epimorphisms (#15123)

TwoFX committed 3 years ago

f0514a8f

feat(algebra/order/positive): new file (#14833)

urkud committed 3 years ago

24a233d4

feat(measure_theory/function/conditional_expectation/basic): add some condexp lemmas (#16273)

kex-y committed 3 years ago

7c4a46f3

feat(data/rat/nnrat): Nonnegative rationals (#16283)

YaelDillies committed 3 years ago

6de241f9

feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167)

sgouezel committed 3 years ago

de62604b

chore(category_theory): fix name of mono_app_of_mono (#16275)

joelriou committed 3 years ago

937c692d

fix(combinatorics/composition): remove non-terminal simp (#16259)

gebner committed 3 years ago

8dd80093

feat(algebra/order/field): Canonically linear ordered semifields (#15677)

YaelDillies committed 3 years ago

1c2d71f1

feat(data/rat/defs): add two lemmas for `pnat_denom` of 0 and 1 (#15864)

joneugster committed 3 years ago

ebb53dc3

chore(category_theory/limits/shapes/finite_products): avoid tidy (#16261)

gebner committed 3 years ago

6901db60

docs(ring_theory/valuation/valuation_subring): clarify value group docstring (#16272)

kbuzzard committed 3 years ago

c241a033

feat(category_theory): coseparators in structured_arrow (#15981)

TwoFX committed 3 years ago

fef8efdf

move lemmas around

kex-y committed 3 years ago

b92e6458

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets. (#15321)

kkytola committed 3 years ago

c95908a6

initial commit sorry free

kex-y committed 3 years ago

2cc1df70

feat(ring_theory/ideal): Two little `restrict_scalars` lemmas (#16248)

Vierkantor committed 3 years ago

18361694

feat(analysis/normed_space/star/spectrum): star algebra morphisms over ℂ are norm contractive (#16219)

j-loreaux committed 3 years ago

5ef64261

feat(data/{list, multiset}/basic): generalize `pmap_congr` (#16220)

astrainfinita committed 3 years ago

15c8fdda

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

leanprover-community-bot committed 3 years ago

3b0a5074

feat(algebra/order/floor): lemmas about `int.floor`, `int.ceil`, `int.fract`, `round` (#16158)

ocfnash committed 3 years ago

b059a442

feat(algebra/order/smul): `positivity` extension for `smul` (#16162)

YaelDillies committed 3 years ago

4ed5f0e1

feat(data/zmod/quotient): Version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption (#16175)

tb65536 committed 3 years ago

3d0bb870

feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_on_filter (#15871)

khwilson committed 3 years ago

b6258037

docs(algebra/field/basic): fix typo (#16241)

jcommelin committed 3 years ago

36e16da1

Newer Older