leanprover-community/mathlib3

Pull Requests Commits

docstring + fix

apnelson1 committed 3 years ago

9e175f62

YaelDillies committed 3 years ago

4e606264

refactor(order/conditionally_complete_lattice): tweak `well_founded.conditionally_complete_linear_order_with_bot` (#14706)

vihdzp committed 3 years ago

29036740

refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463)

riccardobrasca committed 3 years ago

ae5b6952

feat(analysis/normed/group/basic): `isometry.norm_map_of_map_zero` (#14836)

jsm28 committed 3 years ago

10a52752

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

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

Older