leanprover-community/mathlib

Pull Requests Commits

feat(analysis/special_functions): little o behaviour of exp/log at infinity (#11840)

b-mehta committed 3 years ago

a5ffb9b0

fix(catgory_theory/limits): fix a typo (#12341)

TwoFX committed 3 years ago

c4cf451a

feat(ring_theory/witt_vector): Witt vectors are a DVR (#12213)

robertylewis committed 3 years ago

8ef4331c

doc(imo*,algebra/continued_fractions/computation): change \minus to - (#12338)

kbuzzard committed 3 years ago

1dfb38d0

feat(geometry/euclidean/oriented_angle): oriented angles with respect to an orientation (#12236)

jsm28 committed 3 years ago

00a3d02e

feat(data/list/basic): add last'_append and head'_append_of_ne_nil (#12221)

nomeata committed 3 years ago

77e76ee5

feat(logic/function/basic): not_surjective_Type (#12311)

ChrisHughes24 committed 3 years ago

b1c2d70a

chore(category_theory/idempotents): minor suggestions (#12303)

kim-em committed 3 years ago

7ae0b362

feat(set_theory/cardinal): add three_le (#12225)

nomeata committed 3 years ago

07374a27

feat(category_theory/category/Groupoid): Add coercion to sort (#12324)

prakol16 committed 3 years ago

86d686cc

fix(set_theory/ordinal_arithmetic): Fix universes (#12320)

vihdzp committed 3 years ago

907e5ba4

feat(data/quot): primed quotient funcs on `mk` (#12204)

pechersky committed 3 years ago

906a88bd

feat(set_theory/ordinal_arithmetic): Added missing theorems for `lsub` and `blsub` (#12318)

vihdzp committed 3 years ago

4afb8d29

chore(set_theory/ordinal): Minor golf in `card` (#12298)

vihdzp committed 3 years ago

bb9539cf

feat(analysis/normed_space): add `normed_space 𝕜 (uniform_space.completion E)` (#12148)

urkud committed 3 years ago

b4f87d99

refactor(category_theory/eq_to_hom): conjugation by eq_to_hom same as heq (#12025)

Jlh18 committed 3 years ago

abf5dfca

feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group (#11834)

nomeata committed 3 years ago

1fe9708e

chore(linear_algebra/orientation): split into 2 files (#12302)

urkud committed 3 years ago

add068d1

feat(algebra/category/GroupWithZero): The category of groups with zero (#12278)

YaelDillies committed 3 years ago

188b371b

feat(category_theory/idempotents): idempotent completeness and functor categories (#12270)

joelriou committed 3 years ago

163d1a6d

feat(order/category/BoundedLattice): The category of bounded lattices (#12257)

YaelDillies committed 3 years ago

817b4c4b

refactor(topology/compact_open): Remove `locally_compact_space` hypothesis in `continuous_map.t2_space` (#12306)

tb65536 committed 3 years ago

3d8c22fd

feat(category_theory/limits): generalize has_biproduct.of_has_product (#12116)

TwoFX committed 3 years ago

4cf0e600

feat(category_theory/limits): biproducts are unique up to iso (#12114)

TwoFX committed 3 years ago

09ba5304

feat(analysis/convex/integral): strict Jensen's inequality (#11552)

urkud committed 3 years ago

fe6ea3ec

feat(analysis/normed_space/add_torsor): `dist` and `line_map` (#12265)

urkud committed 3 years ago

c8150ccf

feat(algebra/star/pointwise, algebra/star/basic): add pointwise star, and a few convenience lemmas (#12290)

j-loreaux committed 3 years ago

3b49fe25

feat(analysis/normed_space/star/spectrum): prove the spectrum of a unitary element in a C*-algebra is a subset of the unit sphere (#12238)

j-loreaux committed 3 years ago

87fc3eae

feat(topology,analysis): any function is continuous/differentiable on a subsingleton (#12293)

urkud committed 3 years ago

0f1bc2c0

refactor(topology,analysis): use `maps_to` in lemmas like `continuous_on.comp` (#12294)

urkud committed 3 years ago

bfc05842

Newer Older