leanprover-community/mathlib

Pull Requests Commits

feat(topology/instances/ennreal): golf, add lemmas about `supr_add_supr` (#14274)

urkud committed 3 years ago

01eda9ab

feat(logic/hydra): termination of a hydra game (#14190)

alreadydone committed 3 years ago

9861db0d

refactor(algebra/big_operators/*): Generalize to division monoids (#14189)

YaelDillies committed 3 years ago

8304b951

feat(order/atoms): add lemmas (#14162)

urkud committed 3 years ago

16a5286f

chore(set_theory/game/ordinal): minor golfing (#14317)

vihdzp committed 3 years ago

4cdde79f

feat(topology/metric_space): use weaker TC assumptions (#14316)

urkud committed 3 years ago

005df456

feat(algebra/ring/basic): add `no_zero_divisors.to_cancel_comm_monoid_with_zero` (#14302)

eric-wieser committed 3 years ago

9e9a2c9e

chore(logic/equiv/set): golf definition (#14284)

eric-wieser committed 3 years ago

dcb3cb1c

refactor(set_theory/game/nim): `0 ≈ nim 0` → `nim 0 ≈ 0` (#14270)

vihdzp committed 3 years ago

60897e3b

doc(set_theory/game/basic): improve docs (#14268)

vihdzp committed 3 years ago

5a24374d

chore(linear_algebra): generalize conversion between matrices and bilinear forms to semirings (#14263)

eric-wieser committed 3 years ago

cef5898c

refactor(set_theory/cardinal/cofinality): infer arguments (#14251)

vihdzp committed 3 years ago

e09e8770

chore(data/matrix/basic): add `matrix.star_mul_vec` and `matrix.star_vec_mul` (#14248)

eric-wieser committed 3 years ago

d9465730

feat(set_theory/game/pgame): `add_lf_add_of_lf_of_le` (#14150)

vihdzp committed 3 years ago

684587b0

refactor(category_theory/shift): remove opaque_eq_to_iso (#14262)

kim-em committed 3 years ago

b7952ee5

feat(set_theory/surreal/basic): definition of `≤` and `<` on numeric games (#14169)

vihdzp committed 3 years ago

178456ff

feat(set_theory/game/pgame): instances for empty moves of addition (#14297)

vihdzp committed 3 years ago

fe2b5ab0

chore(algebra/geom_sum): rename to odd.geom_sum_pos (#14264)

ericrbg committed 3 years ago

1b7e918c

feat(measure_theory): use more `[(pseudo_)metrizable_space]` (#14232)

urkud committed 3 years ago

eb8994b8

feat(category_theory/natural_isomorphism): a simp lemma cancelling inverses (#14299)

kim-em committed 3 years ago

eae05105

feat(data/real/ennreal): lemmas about unions and intersections (#14296)

urkud committed 3 years ago

e4a8db19

refactor(category_theory): remove some simp lemmas about eq_to_hom (#14260)

kim-em committed 3 years ago

a836c6db

refactor(order/filter/lift): reformulate `lift_infi` etc (#14138)

urkud committed 3 years ago

0386c3b3

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

Newer Older