leanprover-community/mathlib

Pull Requests Commits

urkud committed 3 years ago

aad09852

Merge branch 'master' into card-ccl

urkud committed 3 years ago

17d99ade

feat(topology/algebra/infinite_sum) Sums over Z vs sums over N (#14667)

loefflerd committed 3 years ago

65c9ffb2

feat(group_theory/group_action/sum): Scalar action on a sum of types (#14818)

YaelDillies committed 3 years ago

f460576d

feat(set_theory/game/basic): Basic lemmas on `inv` (#13840)

vihdzp committed 3 years ago

5dabef86

feat(algebra/category/Module): Tannaka duality for rings (#14352)

kim-em committed 3 years ago

69686e71

feat(category_theory/preadditive/eilenberg_moore): (Co)algebras over a (co)monad are preadditive (#14811)

Julian-Kuelshammer committed 3 years ago

7f358d06

feat(set_theory/game/pgame): tweak lemmas (#14810)

vihdzp committed 3 years ago

0a5b9eba

feat(analysis/asymptotics): add several lemmas (#14805)

urkud committed 3 years ago

4264220c

feat(geometry/euclidean/inversion) new file (#14692)

urkud committed 3 years ago

100975e9

feat(topology/metric_space/baire): generalize some lemmas (#14633)

urkud committed 3 years ago

92d5fdf8

feat(tactic/core + test/list_summands): a function extracting a list of summands from an expression (#14617)

adomani committed 3 years ago

f1b0402a

feat(group_theory/torsion): define the p-primary component of a group (#14312)

Julian committed 3 years ago

3a8e0a11

chore(order/pfilter): more `principal` API (#14759)

kbuzzard committed 3 years ago

3abee054

chore(data/nat/lattice): add `nat.infi_of_empty` to match `_root_.infi_of_empty` (#14797)

eric-wieser committed 3 years ago

39986ae2

feat(data/complex/basic): add `complex.abs_le_sqrt_two_mul_max` (#14804)

urkud committed 3 years ago

7fb5ed20

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

Older