leanprover-community/mathlib

Pull Requests Commits

AlexKontorovich committed 3 years ago

c980313c

AlexKontorovich committed 3 years ago

db9c3f2c

AlexKontorovich committed 3 years ago

94e241a7

AlexKontorovich committed 3 years ago

1a6495b7

AlexKontorovich committed 3 years ago

171b0520

AlexKontorovich committed 3 years ago

326de6a8

AlexKontorovich committed 3 years ago

0331aeb0

AlexKontorovich committed 3 years ago

c7926d6a

AlexKontorovich committed 3 years ago

3451cb9a

AlexKontorovich committed 3 years ago

ae641419

AlexKontorovich committed 3 years ago

02bef471

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

Older