leanprover-community/mathlib

Pull Requests Commits

refactor(linear_algebra/exterior_algebra): redefine `exterior_algebra` as `clifford_algebra 0` (#14819)

eric-wieser committed 3 years ago

c1abe061

feat(data/dfinsupp/basic): add missing lemmas about `single` (#14815)

eric-wieser committed 3 years ago

320ea398

feat(algebra/order/pointwise): Supremum of pointwise operations (#13669)

YaelDillies committed 3 years ago

c5e13baa

feat(group_theory/group_action/sigma): Scalar action on a sigma type (#14825)

YaelDillies committed 3 years ago

f9c339ec

chore(algebra/group/basic): lemmas about `bit0`, `bit1`, and addition (#14798)

eric-wieser committed 3 years ago

ff40b2c1

feat(order/filter/bases): basis for directed (b)infi of filters (#14775)

ADedecker committed 3 years ago

df50b88a

feat(number_theory/number_field): add definitions and results about embeddings (#14749)

xroblot committed 3 years ago

2604c048

refactor(analysis/complex/upper_half_plane): move topology to a new file (#14748)

urkud committed 3 years ago

8263a4bf

feat(geometry/manifold/diffeomorph): some additions needed for smooth vector bundles (#14738)

fpvandoorn committed 3 years ago

804afcb0

feat(analysis/convex/join): Join of sets (#14676)

YaelDillies committed 3 years ago

04f45054

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

Newer Older