leanprover-community/mathlib3

Pull Requests Commits

AI experimenting

BoltonBailey committed 3 years ago

c57cf8d3

BoltonBailey committed 3 years ago

8d7a7759

BoltonBailey committed 3 years ago

de52f1d2

BoltonBailey committed 3 years ago

fff12d41

BoltonBailey committed 3 years ago

6ef8aa69

fix line too long

BoltonBailey committed 3 years ago

f0a54ef1

BoltonBailey committed 3 years ago

e2b8ce47

restore old rotate as rotatel

BoltonBailey committed 3 years ago

bdbef77c

change other rotates to match

BoltonBailey committed 3 years ago

961291be

make int rotate the rotate

BoltonBailey committed 3 years ago

7778cb01

BoltonBailey committed 3 years ago

89e91156

BoltonBailey committed 3 years ago

47311e9f

feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

Paul-Lez committed 3 years ago

36e01301

feat(data/nat/{choose/multinomial,factorial/big_operations}): add multinomial coefficient definition with basic lemma's (#16170)

pimotte committed 3 years ago

a280c1e5

chore(linear_algebra): rename dual_pair (#16482)

PatrickMassot committed 3 years ago

1b3556cc

feat(analysis/inner_product_space/pi_L2): change of basis matrix between orthonormal bases is unitary (#16474)

hrmacbeth committed 3 years ago

f058af30

feat(algebra/algebra/basic): add two simp lemmas (#16096)

Paul-Lez committed 3 years ago

38963b53

chore(data/real/cau_seq_completion): golf using existing lemmas (#16469)

eric-wieser committed 3 years ago

60f72157

feat(data/polynomial/algebra_map): add `aeval_X_left_apply` (#16433)

astrainfinita committed 3 years ago

86be023b

feat(analysis/normed/group/seminorm): Group norms (#16237)

YaelDillies committed 3 years ago

28b23c94

feat(data/real/ennreal): Add `to_real_{min, sup, inf}` (#16233)

linesthatinterlace committed 3 years ago

e1847377

refactor(set_theory/basic): match `x < ℵ₀` lemmas with `x ≤ ℵ₀` lemmas (#15662)

vihdzp committed 3 years ago

1c4e1843

feat(linear_algebra/finsupp): A variant of `finsupp.total` for `fintype`s. (#15462)

erdOne committed 3 years ago

d5ef0684

feat(measure_theory/function/conditional_expectation): conditional expectation with respect to the bot sigma algebra (#16342)

RemyDegenne committed 3 years ago

745e23d5

feat(data/{seq,stream}): cons_injective2 (#15832)

vihdzp committed 3 years ago

3c006126

chore(probability/martingale): move the optional stopping theorem to its own file (#16464)

RemyDegenne committed 3 years ago

87714908

refactor(algebra/order/monoid): Remove redundant field from `ordered_cancel_comm_monoid` (#16445)

YaelDillies committed 3 years ago

d04db585

feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#16457)

urkud committed 3 years ago

27917391

feat(data/fintype/basic): `fintype.to_finset_prod` (#16459)

kmill committed 3 years ago

c8c740df

feat(algebra/parity): Primes are not square (#16430)

YaelDillies committed 3 years ago

5e78882f

Older