leanprover-community/mathlib

Pull Requests Commits

chore(topology/uniform_space): use weaker TC assumptions (#12066)

urkud committed 3 years ago

6a09cd06

lower instance priorities

dupuisf committed 3 years ago

42dbbe04

turn `is_star_normal` into a type class

dupuisf committed 3 years ago

d5a6a5ef

feat(topology/algebra): relax some `Type*` assumptions to `Sort*` (#12058)

ADedecker committed 3 years ago

eeb29569

feat (analysis/normed_space/spectrum): prove Gelfand's formula for the spectral radius (#11916)

j-loreaux committed 3 years ago

b0fe9723

feat(category_theory): separators and detectors (#11880)

TwoFX committed 3 years ago

d76ac2e0

feat(combinatorics/simple_graph/connectivity): add functions to split walks and to create paths (#11095)

kmill committed 3 years ago

ff2c9dc3

move(data/nat/choose/bounds): Move from `combinatorics.choose.bounds` (#12051)

YaelDillies committed 3 years ago

5027b283

feat(data/{list,multiset,finset}/nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028)

kmill committed 3 years ago

52aaf173

feat(data/equiv,logic/embedding): add `can_lift` instances (#12049)

urkud committed 3 years ago

c0c673ab

feat(analysis/specific_limits): add `tendsto_zero_smul_of_tendsto_zero_of_bounded` (#12039)

ecstatic-morse committed 3 years ago

c686fcc1

feat(ring_theory/multiplicity): Equality of `factorization`, `multiplicity`, and `padic_val_nat` (#12033)

stuart-presnell committed 3 years ago

6e64492d

feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003)

RemyDegenne committed 3 years ago

9307f5b4

feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` lemmas (#11969)

jsm28 committed 3 years ago

60b77a76

feat(number_theory/zsqrtd/basic): add some lemmas (#11964)

Ruben-VandeVelde committed 3 years ago

0c33309c

feat(set_theory/ordinal_arithmetic): Suprema of functions with the same range are equal (#11910)

vihdzp committed 3 years ago

3d1354ce

refactor(set_theory/ordinal_arithmetic): `omin` → `Inf` (#11867)

vihdzp committed 3 years ago

721bace8

feat(model_theory/finitely_generated): Finitely generated and countably generated (sub)structures (#11857)

awainverse committed 3 years ago

9acc1d40

feat(data/nat/modeq): add modeq and dvd lemmas from Apostol Chapter 5 (#11787)

stuart-presnell committed 3 years ago

41dd6d8a

feat(topology/uniform/uniform_embedding): a sum of two complete spaces is complete (#11971)

sgouezel committed 3 years ago

b0508f3c

feat(order/category/Lattice): The category of lattices (#11968)

YaelDillies committed 3 years ago

77ca1ed3

feat(number_theory/cyclotomic/zeta): add lemmas (#11786)

riccardobrasca committed 3 years ago

5bcffd96

feat(order/complete_boolean_algebra): Frames (#11709)

YaelDillies committed 3 years ago

a2d7b55a

feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)

ADedecker committed 3 years ago

440e6b3b

feat(group_theory/nilpotent): products of nilpotent groups (#11827)

nomeata committed 3 years ago

c5578f91

feat(topology/algebra): weaken typeclasses to only require `has_continuous_const_smul` (#11995)

eric-wieser committed 3 years ago

f12b3d91

chore(category_theory/triangulated/rotate): optimizing some proofs (#12031)

arthurpaulino committed 3 years ago

f1334b95

chore(probability_theory/*): Rename folder (#11989)

YaelDillies committed 3 years ago

4c76eac9

chore(scripts): update nolints.txt (#12048)

leanprover-community-bot committed 3 years ago

430faa98

feat(analysis/inner_product_space/adjoint): `is_self_adjoint_iff_eq_a… (#12047)

hparshall committed 3 years ago

a1283d0b

Newer Older