leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

7b9489cb

working default values

eric-wieser committed 3 years ago

5731065c

add the target code to generate

eric-wieser committed 3 years ago

ede937c2

Merge remote-tracking branch 'origin/eric-wieser/to_json' into eric-wieser/to_json-default

eric-wieser committed 3 years ago

aa02ec8f

generalize level

eric-wieser committed 3 years ago

393bcb27

eric-wieser committed 3 years ago

1f66023b

eric-wieser committed 3 years ago

c0fb1a08

fix Prop fields

eric-wieser committed 3 years ago

7db041e7

eric-wieser committed 3 years ago

f908b5ea

eric-wieser committed 3 years ago

19f3ead0

eric-wieser committed 3 years ago

b79acbd8

eric-wieser committed 3 years ago

561c4c98

feat(data/json): helper functions for json serialization

eric-wieser committed 3 years ago

59985468

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

Older