leanprover-community/mathlib3

Pull Requests Commits

simp lemmas from companion def

pbazin committed 3 years ago

3a57527c

pbazin committed 3 years ago

45a00561

pbazin committed 3 years ago

ba2ccf27

pbazin committed 3 years ago

32ffa13c

companion matrix

pbazin committed 3 years ago

e229016a

feat(topology/metric_space/metrizable): assume `regular_space` (#14586)

urkud committed 3 years ago

4a4cd6d6

chore(set_theory/game/basic): spacing tweaks + fix docstring typo (#14580)

vihdzp committed 3 years ago

de648fd5

feat(set_theory/game/pgame): induction on left/right moves of add/mul (#14345)

vihdzp committed 3 years ago

6ad1a55f

feat(measure_theory/measure/measure_space): add `interval_oc_ae_eq_interval` (#14566)

urkud committed 3 years ago

c7a1319b

chore(geometry/manifold/charted_space): make `M` an explicit argument (#14562)

urkud committed 3 years ago

2c893060

refactor(analysis/asymptotics): rename `is_O.join` to `is_O.sup` (#14558)

urkud committed 3 years ago

d0b7ecc9

feat(order/liminf_limsup): add a few lemmas (#14554)

urkud committed 3 years ago

2b7e72b0

refactor(../metric_space/baire): add baire_space class and instances (#14547)

D-Thomine committed 3 years ago

029a9551

feat(analysis/normed_space/banach): closed graph theorem (#14265)

ADedecker committed 3 years ago

d28aa2c9

feat(algebra/order/*): typeclass for `0 ≤ 1` (#14510)

vihdzp committed 3 years ago

7b7da893

feat(measure_theory/measure/finite_measure_weak_convergence): Prove one implication of portmanteau theorem, convergence implies a limsup condition for measures of closed sets. (#14116)

kkytola committed 3 years ago

abbc7f63

feat(analysis/convex/krein_milman): The Krein-Milman theorem (#8112)

YaelDillies committed 3 years ago

d6477a89

move(set_theory/ordinal/cantor_normal_form): move `CNF` to a new file (#14563)

vihdzp committed 3 years ago

d490ad10

feat(order/antichain, order/minimal): some antichain lemmas (#14507)

apnelson1 committed 3 years ago

0f5ea396

chore(linear_algebra/std_basis): minor golfs (#14552)

eric-wieser committed 3 years ago

d88ecd5b

feat(algebra/char_p): add two helper lemmas about the cast of the characteristics being zero (#14464)

Jon Eugster committed 3 years ago

789af09c

feat(set_theory/*) `cardinal.min` → `Inf` (#13410)

vihdzp committed 3 years ago

769a9349

feat(data/nat/factorization): Lemma on zero-ness of factorization (#14560)

Smaug123 committed 3 years ago

736b4e5c

feat(src/analysis/normed_space): various improvements for continuous bilinear maps (#14539)

fpvandoorn committed 3 years ago

043fa29d

feat(analysis/normed_space/hahn-banach/separation): Eidelheit's theorem (#14460)

YaelDillies committed 3 years ago

d9e72ffb

refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467)

vihdzp committed 3 years ago

b6395b3a

chore(set_theory/cardinal/cofinality): golf + fix spacing (#14509)

vihdzp committed 3 years ago

8651b707

refactor(group_theory/group_action/defs): rename has_faithful_scalar (#14515)

berndlosert committed 3 years ago

10f45725

feat(set_theory/cardinal/cofinality): weaker definition for regular cardinals (#14433)

vihdzp committed 3 years ago

157013da

feat(data/fin/tuple/monotone): new file (#14483)

urkud committed 3 years ago

741f4deb

Older