leanprover-community/mathlib

Pull Requests Commits

rebuild the cache please

eric-wieser committed 3 years ago

c783cc6b

eric-wieser committed 3 years ago

fa3d72bf

add nonconstructive approach

eric-wieser committed 3 years ago

5501d2c2

eric-wieser committed 3 years ago

c5a0a4ed

refactor(algebra/direct_sum/module): use `decomposition` instead of `is_internal` when the equiv is needed

eric-wieser committed 3 years ago

e5221a1b

feat(linear_algebra/alternating): add more compositional API (#14802)

eric-wieser committed 3 years ago

bd6b98b2

chore(order/symm_diff): add lemma about `bxor` (#14801)

eric-wieser committed 3 years ago

0c476570

feat(analysis/complex/basic): add a few lemmas about `dist` on `complex` (#14796)

urkud committed 3 years ago

4ff9e93e

feat(data/set/intervals): add two `ssubset` lemmas (#14793)

urkud committed 3 years ago

d2369bcb

feat(algebra/algebra/basic) : add ring_hom.equiv_rat_alg_hom (#14772)

xroblot committed 3 years ago

e23de85c

feat(order/topology/**/uniform*): Lemmas about uniform convergence (#14587)

khwilson committed 3 years ago

260d472e

feat(category_theory/monad/kleisli): dualise kleisli of monad to cokleisli of comonad (#14799)

Julian-Kuelshammer committed 3 years ago

545f0fb9

refactor(linear_algebra/quadratic_form/basic): generalize to semiring (#14303)

eric-wieser committed 3 years ago

ade72abc

feat(group_theory/sylow): API lemmas for smul and subtype (#14521)

tb65536 committed 3 years ago

9c2b8903

feat(data/list/of_fn): Add `list.of_fn_add` and `list.of_fn_mul` (#14370)

eric-wieser committed 3 years ago

0be36f6f

feat(set/basic, order/boolean_algebra): generalized `compl_comp_compl` (#14784)

apnelson1 committed 3 years ago

e427a0e5

feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599)

vihdzp committed 3 years ago

d21469e4

feat(set_theory/{pgame, basic}): Notation for `relabelling`, golfing (#14155)

vihdzp committed 3 years ago

d0b93faf

feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626)

eric-wieser committed 3 years ago

ae10dced

feat(analysis/inner_product_space): Gram-Schmidt Basis (#14514)

abentkamp committed 3 years ago

67da2721

fix(data/rat/basic): Remove incorrect simp attribute (#14765)

Jon Eugster committed 3 years ago

988f160d

feat(linear_algebra/clifford_algebra/fold): Add recursors for folding along generators (#14619)

eric-wieser committed 3 years ago

6c46641d

feat(set_theory/game/ordinal): addition of ordinals on games matches natural addition (#14298)

vihdzp committed 3 years ago

7584a104

feat(data/nat/basic): add a few lemmas (#14718)

user7230724 committed 3 years ago

b05d8459

feat(algebra/homology,category_theory/abelian): exact_comp_mono_iff (#14410)

TwoFX committed 3 years ago

3feb151c

feat(analysis/asymptotics): define `is_Theta` (#14567)

urkud committed 3 years ago

6834a24e

feat(analysis/special_functions/arsinh): add lemmas, review API (#14668)

urkud committed 3 years ago

0053e3c5

refactor(set_theory/game/*): Delete `winner.lean` (#14271)

vihdzp committed 3 years ago

22f32559

chore(*): Bump to Lean 3.43.0 (#14684)

urkud committed 3 years ago

f991b4d4

feat(data/polynomial/erase_lead): `lt_nat_degree_of_mem_erase_lead_support` (#14745)

tb65536 committed 3 years ago

c81c6c91

Older