leanprover-community/mathlib3

Pull Requests Commits

Revert "fix timeouts"

kim-em committed 3 years ago

23cd34bb

kim-em committed 3 years ago

933620c0

feat(topology/metric_space/basic): a continuous function is bounded on a neighborhood of a compact set (#17457)

sgouezel committed 3 years ago

08a8fd81

feat(geometry/euclidean/angle/oriented/affine): midpoint lemmas (#17444)

jsm28 committed 3 years ago

75351039

feat(analysis/[seminorm, locally_convex/with_seminorms]): semilinearize `seminorm.comp` (#17286)

ADedecker committed 3 years ago

a990661d

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964)

j-loreaux committed 3 years ago

b75fd415

feat(topology/uniform_space): ulift as a uniform equiv (#17451)

sgouezel committed 3 years ago

1499a80b

chore(algebra/parity): Reduce imports (#17391)

YaelDillies committed 3 years ago

54c432da

chore(analysis/calculus/fderiv): squeeze simps (#17344)

mcdoll committed 3 years ago

8f5cf785

fix(analysis/normed_space/pi_Lp): remove bad simp lemmas for `pi_Lp.equiv` (#17327)

eric-wieser committed 3 years ago

9dffb788

feat(*): define classes for coercions that are homomorphisms (#17048)

Vierkantor committed 3 years ago

6965ed89

chore(analysis/normed_space/operator_norm): add missing lemma (#17449)

mcdoll committed 3 years ago

bfb15ebd

refactor(linear_algebra,analysis/normed_space): use `finite`, review API, golf (#17320)

urkud committed 3 years ago

d9a51803

feat(ring_theory): specialize Chinese Remainder Theorem to two ideals (#17189)

Vierkantor committed 3 years ago

a9dd84b4

feat(combinatorics/simple_graph/connectivity): `fintype G.connected_component` and `decidable G.connected` (#17148)

kmill committed 3 years ago

69d5021b

chore(topology/*): rename compact_univ to is_compact_univ, and many more (#17436)

sgouezel committed 3 years ago

27929793

feat(analysis/convex/jensen): Maximum modulus principle for finsets (#17091)

YaelDillies committed 3 years ago

bfad3f45

chore(field_theory): move `polynomial.splits` to a new file (#17354)

Vierkantor committed 3 years ago

6a5a6494

chore(data/nat/basic): drop some `nat`-specific lemmas (#17400)

urkud committed 3 years ago

6b921b20

refactor(data/rat/defs): Use `int.cast` instead of `rat.of_int` (#17392)

YaelDillies committed 3 years ago

c18a48e9

refactor(topology/sheaf_condition): remove redundant constructions (#17378)

alreadydone committed 3 years ago

85d6221d

feat(category_theory/extensive): Define extensive categories (#17318)

erdOne committed 3 years ago

a6d9c65a

feat(data/finsupp/basic): add a `has_repr` instance (#17283)

eric-wieser committed 3 years ago

64444a2d

feat(analysis/normed/group/basic): `dist (a * b) b` (#17240)

YaelDillies committed 3 years ago

4a681f15

feat(algebraic_geometry/open_immersion): `is_open_immersion.lift_app` (#17186)

erdOne committed 3 years ago

ea469516

feat(algebra/module/localized_module): Add `is_localized_module.mk'`. (#17064)

erdOne committed 3 years ago

fb63d2da

feat(order/zorn): Variant for `Ici` (#17053)

YaelDillies committed 3 years ago

fc6a9d12

refactor(data/finset/prod): make arguments to `mem_diag` and `mem_off_diag` implicit (#16314)

YaelDillies committed 3 years ago

bb8b0fd0

feat(data/{multiset/dedup, finset/basic}): add some lemmas about `multiset.dedup` (#16230)

astrainfinita committed 3 years ago

937a36ee

feat(representation_theory/character): orthogonality of characters (#16043)

antoinelab01 committed 3 years ago

55b3f820

Newer Older