Commits leanprover-community/mathlib

feat(data/fin/basic): eq_succ_of_ne_zero, coe_cast_pred, succ_pred_above_succ (#16294)

joelriou committed 3 years ago

b799b43d

feat(data/nat/parity): add lemmas nat.bit{0|1}_mod_bit0 (#16396)

MichaelStollBayreuth committed 3 years ago

3c227fc0

chore(category_theory/*): Lint (#16366)

YaelDillies committed 3 years ago

3f409bd9

feat(data/finsupp/ne_locus): add a not-member lemma (#16245)

adomani committed 3 years ago

b3b5475d

feat(category_theory/sites/sheaf): category of sheaf is preadditive when target is preadditive (#16324)

jjaassoonn committed 3 years ago

a67ec23d

chore(algebra/order/ring): golf a few proofs (#16398)

urkud committed 3 years ago

fbebf1a0

feat(category_theory/limits/shapes/products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180)

jjaassoonn committed 3 years ago

e11bafa5

feat(measure_theory/measure/measure_space): add variants of `ae_restrict_Union_eq` (#16370)

RemyDegenne committed 3 years ago

f0c55c2a

feat(src/data/*): lemmas about emptiness for finset/multiset/vector coercions (#16113)

dtumad committed 3 years ago

58903102

refactor(order/rel_classes): ditch `is_strict_total_order'` (#16069)

vihdzp committed 3 years ago

1ef34126

feat(algebra/monoid_algebra/no_zero_divisors): left/right order implies no zero divisors (#16299)

adomani committed 3 years ago

3e067975

chore(analysis/analytic/isolated_zeros): tidy exists_has_sum_smul_of_apply_eq_zero (#16389)

Ruben-VandeVelde committed 3 years ago

c3762602

feat(algebra/group_power/basic): add `pow_mul_pow_eq_one` (#16328)

astrainfinita committed 3 years ago

03773179

feat(linear_algebra/affine_space/affine_subspace): `vadd_mem_iff_mem_of_mem_direction` (#16383)

jsm28 committed 3 years ago

d25f4d64

feat(topology/instances/nnreal): add `nnreal.pow_order_iso` (#16344)

urkud committed 3 years ago

8ac7e3ba

chore(category_theory/sites/compatible_plus): speed up ι_plus_comp_iso_hom (#16379)

Ruben-VandeVelde committed 3 years ago

3f772d42

feat(measure_theory/integral/circle_integral_transform.lean): name ch… (#16387)

CBirkbeck committed 3 years ago

7df02f87

refactor(linear_algebra/affine_space/finite_dimensional): change three lemmas to instances (#16331)

jsm28 committed 3 years ago

06930844

feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290)

MichaelStollBayreuth committed 3 years ago

4b4975cf

feat(order/heyting/boundary): Co-Heyting boundary (#16257)

YaelDillies committed 3 years ago

0ab31714

feat(tactic/positivity): Handle division of integers (#16163)

YaelDillies committed 3 years ago

3a8665a8

feat(probability/martingale/basic): the stopped process of a submartingale is a submartingale (#16375)

RemyDegenne committed 3 years ago

44c90247

feat(linear_algebra/ray): `same_ray_map_iff` for injective linear maps (#16377)

jsm28 committed 3 years ago

dc8113b0

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

leanprover-community-bot committed 3 years ago

9b11656c

feat(geometry/euclidean/basic): `affine_isometry.angle_map` (#16374)

jsm28 committed 3 years ago

e1d2f5bd

chore(data/nat/part_enat): make `coe_inj` `@[norm_cast]` (#16334)

astrainfinita committed 3 years ago

7fdc06de

feat(order/filter/at_top_bot): add lemmas about convergence of `λ x, r * f x` to `±∞` (#16355)

urkud committed 3 years ago

7ce2bb4a

fix(algebra/category/Module): speedup (#16371)

collares committed 3 years ago

86ee6689

doc(data/nat/{part_enat, lattice}): update doc string (#16345)

astrainfinita committed 3 years ago

075b0d23

feat(analysis/special_functions/stirling): Stirling's formula, part I (#14874)

mo271 committed 3 years ago

a3e847c0