leanprover-community/mathlib

Pull Requests Commits

First full proof

TwoFX committed 3 years ago

be99a5a6

A promising start

TwoFX committed 3 years ago

e4db37b7

feat(algebra/order/monoid) Add zero_le_three and zero_le_four (#15219)

Multramate committed 3 years ago

f51aaab3

feat(data/finset/lattice): add three*2 lemmas about `finset.max/min` (#15212)

adomani committed 3 years ago

e5b8d09b

feat(data/pnat/basic): `succ` as an order isomorphism between `ℕ` and `ℕ+` (#15183)

vihdzp committed 3 years ago

5305d39a

feat(order/filter/ultrafilter): `pure`, `map`, and `comap` lemmas (#15187)

YaelDillies committed 3 years ago

37c27774

feat(linear_algebra/unitary_group): better constructor (#15209)

hrmacbeth committed 3 years ago

861589f2

chore(set_theory/ordinal/arithmetic): review cast API (#14757)

vihdzp committed 3 years ago

983fdd6b

feat(set_theory/ordinal/basic): order type of naturals is `ω` (#15178)

vihdzp committed 3 years ago

6d245b26

feat(combinatorics/simple_graph/subgraph): add `subgraph.comap` and subgraph of subgraph coercion (#14877)

kmill committed 3 years ago

7cf0ae6a

Removed unnecessary assumption in `map_injective_of_injective` (#15184)

nick-kuhn committed 3 years ago

d3d35395

feat(logic/equiv/set): define `equiv.set.pi` (#15176)

urkud committed 3 years ago

f26a0a35

feat(analysis/locally_convex/basic): a few lemmas about balanced sets (#14876)

mcdoll committed 3 years ago

c5b6fe54

feat(set_theory/ordinal/arithmetic): tweak `type_add` and `type_mul` (#15193)

vihdzp committed 3 years ago

fefd449d

feat(analysis/normed_space/star/basic): make starₗᵢ apply to normed star groups (#15173)

j-loreaux committed 3 years ago

f39bd5f0

feat(combinatorics/simple_graph/hasse): The Hasse diagram of `α × β` (#14978)

YaelDillies committed 3 years ago

8a38a697

feat(combinatorics/additive/ruzsa_covering): The Ruzsa covering lemma (#14697)

YaelDillies committed 3 years ago

1a54e4da

chore(data/zmod/defs): shuffle files around (#15142)

ericrbg committed 3 years ago

2d5b45c8

feat(data/rat/defs): add denominator as pnat (#15101)

Jon Eugster committed 3 years ago

11cdccb8

chore(data/nat/squarefree): fix a tactic doc typo for norm num extension (#15189)

alexjbest committed 3 years ago

feb34df6

fix(data/fintype/basic): move card_subtype_mono into the fintype namespace (#15185)

linesthatinterlace committed 3 years ago

5a5d2909

feat(analysis/normed_space/lp_space): normed_algebra structure (#15086)

eric-wieser committed 3 years ago

1937dff0

doc(tactic/wlog): use markdown lists rather than indentation (#15113)

eric-wieser committed 3 years ago

e74e5349

feat(topology/metric_space/hausdorff_distance): Thickening a compact inside an open (#14926)

YaelDillies committed 3 years ago

0bc51f02

feat(combinatorics/simple_graph/prod): Box product (#14867)

YaelDillies committed 3 years ago

93be74b1

feat(data/finset/basic): Coercion of a product of finsets (#15011)

YaelDillies committed 3 years ago

7c070c4d

feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970)

eric-wieser committed 3 years ago

d34b3306

chore(topology/algebra/semigroup): golf file (#14957)

vihdzp committed 3 years ago

563a51af

feat(topology/algebra/uniform_group): `uniform_group` is preserved by Inf and comap (#14889)

ADedecker committed 3 years ago

ba9f346a

refactor(set_theory/cardinal/basic): migrate from `fintype` to `finite` (#15175)

urkud committed 3 years ago

6eeb941c

Older