leanprover-community/mathlib

Pull Requests Commits

urkud committed 3 years ago

668fb9cf

Merge branch 'master' into YK-with-top-le

urkud committed 3 years ago

01daab3f

feat(data/nat/parity): `nat.bit1_div_bit0` (#15268)

tb65536 committed 3 years ago

89a80e67

chore(*): improve some definitional equalities (#15083)

urkud committed 3 years ago

9c400932

feat(data/nat/basic): add `strong_sub_recursion` and `pincer_recursion` (#15061)

stuart-presnell committed 3 years ago

eb091f87

feat(set_theory/game/pgame): strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` (#15255)

vihdzp committed 3 years ago

13f04ec6

feat(algebra/module/torsion): `R/I`-module structure on `M/IM`. (#15092)

erdOne committed 3 years ago

0d659de3

feat(order/order_iso_nat): generalize `well_founded.monotone_chain_condition` to preorders (#15073)

vihdzp committed 3 years ago

fef5124e

feat(representation_theory/character): formula for the dimension of the invariants in terms of the character (#15084)

antoinelab01 committed 3 years ago

119e166b

feat(order/well_founded_set): any relation is well-founded on `Ø` (#15266)

vihdzp committed 3 years ago

aadba9b2

feat(set_theory/game/pgame): `is_option (-x) (-y) ↔ is_option x y` (#15256)

vihdzp committed 3 years ago

6c5e9fe2

feat(set_theory/game/pgame): add `equiv.comm` (#15254)

vihdzp committed 3 years ago

087bc1f9

chore(set_theory/ordinal/cantor_normal_form): mark `CNF` as `pp_nodot` (#15228)

vihdzp committed 3 years ago

2bca4d61

feat(algebra/order/monoid_lemmas_zero_lt): add missing lemmas (#14770)

astrainfinita committed 3 years ago

8284c00e

chore(logic/is_empty): add lemmas for subtype, sigma, and psigma (#15134)

eric-wieser committed 3 years ago

30daa3c0

feat(probability/moments): Chernoff bound on the upper/lower tail of a real random variable (#15129)

RemyDegenne committed 3 years ago

a8fdd990

feat(probability/independence): two tuples indexed by disjoint subsets of an independent family of r.v. are independent (#15131)

RemyDegenne committed 3 years ago

0039a198

feat(tactic/lint): add a linter for `[fintype _]` assumptions (#15202)

urkud committed 3 years ago

d6d3d61e

feat(tactic/polyrith): a tactic using Sage to solve polynomial equalities with hypotheses (#14878)

dhruvbhatia00 committed 3 years ago

423a8b92

chore(set_theory/game/ordinal): minor golf (#15253)

vihdzp committed 3 years ago

1f3c2c09

doc(set_theory/game/pgame): divide file into sections (#15250)

vihdzp committed 3 years ago

623a658f

feat(representation_theory/monoid_algebra_basis): add some API for `k[G^n]` (#14308)

Amelia Livingston committed 3 years ago

52d4daef

fix(.github/workflows): temporarily increase timeout (#15251)

digama0 committed 3 years ago

00dbc7b2

refactor(data/nat/enat): rename `enat` to `part_enat` (#15235)

urkud committed 3 years ago

201d2c61

feat(order/hom/basic): `order_iso` to `rel_iso (<) (<)` (#15182)

vihdzp committed 3 years ago

44905df5

feat(combinatorics/simple_graph/connectivity): simp confluence (#15153)

kmill committed 3 years ago

0f56b2df

fix(order/basic): fix `subtype.linear_order` (#15056)

urkud committed 3 years ago

9a2e5c8b

feat(category_theory): left-exact functors preserve finite limits (#14026)

javra committed 3 years ago

bbe25d4d

feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222)

YaelDillies committed 3 years ago

d3f5adb0

feat(order/modular_lattice): Semimodular lattices (#11602)

YaelDillies committed 3 years ago

888caf7d

Older