leanprover-community/mathlib

Pull Requests Commits

feat(analysis/complex/upper_half_plane): add `upper_half_plane.mk` (#14795)

urkud committed 3 years ago

cf118ee6

chore(algebraic_geometry/function_field): fix timeout in `function_field.algebra` (#14830)

alreadydone committed 3 years ago

26279c5f

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

adomani committed 3 years ago

4cc17909

Merge branch 'aa_sort' of ssh://github.com/leanprover-community/mathlib into aa_sort

adomani committed 3 years ago

0785b946

Merge branch 'master' into aa_sort

adomani committed 3 years ago

29828236

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

vihdzp committed 3 years ago

0a5b9eba

Update src/tactic/move_add.lean

adomani committed 3 years ago

Verified 07f76869

Merge branch 'adomani_list_summands' into aa_sort

adomani committed 3 years ago

83621694

Merge branch 'master' into aa_sort

adomani committed 3 years ago

9660bedc

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

Newer Older