leanprover-community/mathlib

Pull Requests Commits

feat(set_theory/game/pgame): make `lt_iff_le_and_lf` true by def-eq (#14983)

vihdzp committed 4 years ago

0b18823c

refactor(order/upper_lower): Reverse the order on `upper_set` (#14982)

YaelDillies committed 4 years ago

894f92bc

feat(combinatorics/simple_graph/clique): The set of cliques (#14827)

YaelDillies committed 4 years ago

f63d925e

refactor(set_theory/cardinal/*): `cardinal.sup` → `supr` (#14569)

vihdzp committed 4 years ago

f2b108e8

feat(data/nat/totient): more general multiplicativity lemmas for totient (#14842)

stuart-presnell committed 4 years ago

33112c45

feat(analysis/convex/stone_separation): Stone's separation theorem (#14677)

YaelDillies committed 4 years ago

381733a5

docs(linear_algebra/invariant_basis_number): Drop a TODO (#14973)

urkud committed 4 years ago

4111ed94

feat(analysis/special_functions/trigonometric/angle): topology (#14969)

jsm28 committed 4 years ago

ca070dd6

feat(set_theory/surreal/basic): add `numeric.mk` lemma, golf (#14962)

vihdzp committed 4 years ago

28a6f0ac

feat(combinatorics/catalan): definition and equality of recursive and explicit definition (#14869)

Julian-Kuelshammer committed 4 years ago

54352be4

feat({data/{finset,set},order/filter}/pointwise): Missing `smul_comm_class` instances (#14963)

YaelDillies committed 4 years ago

ee7a8863

feat: `add_monoid_with_one`, `add_group_with_one` (#12182)

gebner committed 4 years ago

32b08ef8

feat(data/zmod/algebra): add subsingleton instance for zmod-algebras (#14946)

ericrbg committed 4 years ago

871fcd87

feat(set_theory/ordinal/notation): fast growing hierarchy (#14072)

digama0 committed 4 years ago

e0ecaa9e

feat(data/{finset,set}/basic): More `∪`/`∩` laws (#14952)

YaelDillies committed 4 years ago

cfbb97f7

feat(data/set/lattice): Preimages are disjoint iff the sets are disjoint (#14951)

YaelDillies committed 4 years ago

ccb1cf38

feat(order/symm_diff): The symmetric difference is involutive (#14959)

YaelDillies committed 4 years ago

72cff840

refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448)

YaelDillies committed 4 years ago

b8c3e61b

feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816)

YaelDillies committed 4 years ago

7ee73e4a

feat(algebra/field/basic): Semifields (#14683)

YaelDillies committed 4 years ago

88127521

feat(analysis/normed*): add instances about balls and spheres (#14808)

urkud committed 4 years ago

f9571f0f

chore(*): golf (#14939)

urkud committed 4 years ago

6f923bd9

feat(linear_algebra/clifford_algebra/of_alternating): extend alternating maps to the exterior algebra (#14803)

eric-wieser committed 4 years ago

07c83c81

feat(representation_theory/character): characters of representations (#14453)

antoinelab01 committed 4 years ago

4fd263ba

feat(algebra/indicator_function): add an apply version of `mul_indicator_finset_bUnion` (#14919)

kex-y committed 4 years ago

8bf85d74

feat(probability/martingale): add some lemmas for submartingales (#14904)

kex-y committed 4 years ago

f94a64f7

feat(topology/metric_space): a countably generated uniformity is metrizable (#14052)

urkud committed 4 years ago

40fa2d84

refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848)

urkud committed 4 years ago

fe322e12

feat(linear_algebra/{multilinear, alternating}): add `cod_restrict` and lemmas (#14927)

eric-wieser committed 4 years ago

0e5f278d

feat(data/finite/basic): add missing instances (#14913)

urkud committed 4 years ago

3e326fcb

Newer Older