leanprover-community/mathlib

Pull Requests Commits

feat(probability/stopping): prove measurability of the stopped value (#14062)

RemyDegenne committed 3 years ago

d036d3cf

feat(analysis/convex/uniform): Uniformly convex spaces (#13480)

YaelDillies committed 3 years ago

49b68e80

feat(measure_theory/measure/measure_space): add some `null_measurable_set` lemmas (#14293)

urkud committed 3 years ago

ac006036

feat(set_theory/ordinal/arithmetic): Lemmas about `bsup o.succ f` on a monotone function (#14289)

vihdzp committed 3 years ago

726b9ce7

feat(measure_theory): add `restrict_inter_add_diff` and `lintegral_inter_add_diff` (#14280)

urkud committed 3 years ago

e99ff889

feat(order/filter): add lemmas about filter.has_antitone_basis (#14131)

urkud committed 3 years ago

2d9f791d

refactor(category_theory): remove all decidability instances (#14046)

kim-em committed 3 years ago

52df6ab6

feat(measure_theory/constructions/borel_space): add `norm_cast` lemmas (#14295)

urkud committed 3 years ago

37647bf2

chore(algebra/order/ring): golf `mul_le_one` (#14245)

stuart-presnell committed 3 years ago

9b8588af

feat(ring_theory/valuation/basic): notation for `with_zero (multiplicative ℤ)` (#14064)

ocfnash committed 3 years ago

49ce9677

feat(order/lattice): add `left_lt_inf` etc (#14152)

urkud committed 3 years ago

a8a211f2

feat(set_theory/game/birthday): More basic birthdays (#14287)

vihdzp committed 3 years ago

d8b6f768

chore(data/set/pointwise): Move into the `set` namespace (#14281)

YaelDillies committed 3 years ago

f04684f4

feat({data/finset,order/filter}/pointwise): Multiplicative action on pointwise monoids (#14214)

YaelDillies committed 3 years ago

fc19a4e4

chore(tactic/cancel_denoms): remove an unused have (#14269)

adomani committed 3 years ago

eaa771fc

feat(algebra/big_operators): add `finset.prod_comm'` (#14257)

urkud committed 3 years ago

d787d499

feat(algebra/divisibility): `is_refl` and `is_trans` instances for divisibility (#14240)

vihdzp committed 3 years ago

3fc6fbb3

feat(data/polynomial/mirror): `mirror` is injective (#14254)

tb65536 committed 3 years ago

0e095f0e

feat(set_theory/game/pgame): `sub_self_equiv` (#14272)

vihdzp committed 3 years ago

d217e1db

refactor(set_theory/cardinal/*): add `succ_order` instance, rename `succ` lemmas (#14244)

vihdzp committed 3 years ago

a6b90beb

feat(linear_algebra/trace): trace of projection maps (#14165)

antoinelab01 committed 3 years ago

113f7e42

feat(data/zmod/basic): If the orbit is finite, then the minimal period is positive (#14201)

tb65536 committed 3 years ago

1983e40a

chore(measure_theory/integral/lebesgue): golf some proofs (#14256)

urkud committed 3 years ago

846ed9f2

feat(set_theory/game/pgame): Tweak `pgame.add` API (#13611)

vihdzp committed 3 years ago

180d9751

feat(algebra/algebra/operations): add right induction principles for power membership (#14219)

eric-wieser committed 3 years ago

1483eca1

feat(linear_algebra/trace): trace of prod_map (#13872)

antoinelab01 committed 3 years ago

1e011e3f

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

leanprover-community-bot committed 3 years ago

735fbe05

feat(data/polynomial/mirror): `mirror_eq_iff` (#14238)

tb65536 committed 3 years ago

a5878bbe

refactor(category_theory/discrete): make discrete irreducible (#13762)

kim-em committed 3 years ago

c9c9fa15

feat (algebra/group/prod): Showing that embed_product is injective (#14247)

laughinggas committed 3 years ago

5cf7a1c5

Newer Older