leanprover-community/mathlib

Pull Requests Commits

feat(combinatorics/set_family/harris_kleitman): The Harris-Kleitman inequality (#14497)

YaelDillies committed 3 years ago

35363471

feat(order/bounded_order): Codisjointness (#14195)

YaelDillies committed 3 years ago

f5170fc5

feat(analysis/special_functions/pow): Rational powers are dense (#15002)

YaelDillies committed 3 years ago

b7148c4e

feat(data/nat/basic): split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas (#15099)

stuart-presnell committed 3 years ago

e3e4cc66

feat(algebra/category/BoolRing): The equivalence between Boolean rings and Boolean algebras (#15019)

YaelDillies committed 3 years ago

67779f73

refactor(data/finset/lattice): respell `finset.max/finset.min` using `sup/inf coe` (#15217)

adomani committed 3 years ago

b18b71c4

feat(category_theory/limits): opposites of limit pullback cones (#14526)

joelriou committed 3 years ago

ad080011

feat(set_theory/zfc): simp lemmas for `arity` and `const` (#15214)

vihdzp committed 3 years ago

f4f0f67b

feat(set_theory/zfc): basic lemmas on `pSet.equiv` (#15211)

vihdzp committed 3 years ago

cf4783fe

lint(topology/algebra/order/basic): use `finite` instead of `fintype` (#15203)

urkud committed 3 years ago

4b6ec60f

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

Newer Older