leanprover-community/mathlib

Pull Requests Commits

gebner committed 3 years ago

4f65a631

gebner committed 3 years ago

ce8a6882

gebner committed 3 years ago

82596832

gebner committed 3 years ago

1ec25e9c

gebner committed 3 years ago

412013be

gebner committed 3 years ago

e94a1c22

gebner committed 3 years ago

7ff23d27

s/has_nat_cast/add_monoid_with_one/g

gebner committed 3 years ago

bdc060b4

gebner committed 3 years ago

c2c26e12

gebner committed 3 years ago

93a77bd6

oldstructure metric space

gebner committed 3 years ago

b7d959a4

gebner committed 3 years ago

5e32d7be

gebner committed 3 years ago

7dfb3eda

gebner committed 3 years ago

5309072c

gebner committed 3 years ago

189a0d9b

gebner committed 3 years ago

1fc12b7c

gebner committed 3 years ago

b9623262

gebner committed 3 years ago

e2d33708

gebner committed 3 years ago

1cbefa86

gebner committed 3 years ago

28d48f6e

gebner committed 3 years ago

c78f6f3e

gebner committed 3 years ago

bab7b189

gebner committed 3 years ago

9e2730af

gebner committed 3 years ago

4d612e0c

feat(data/pi): provide `pi.mul_single` (#11849)

nomeata committed 3 years ago

024aef0b

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935)

eric-wieser committed 3 years ago

8c60a927

chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for `inv` (#11959)

j-loreaux committed 3 years ago

fbfdff7e

chore(algebra/star): generalize star_bit0, add star_inv_of (#11951)

eric-wieser committed 3 years ago

ae14f6ad

feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876)

Sebastian-Monnet committed 3 years ago

0227820c

refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871)

vihdzp committed 3 years ago

73513580

Older