leanprover-community/mathlib

Pull Requests Commits

kim-em committed 3 years ago

aa72def5

refactor(order/bounds): don't depend on ordered algebra hierarchy

kim-em committed 3 years ago

d6e5d9df

kim-em committed 3 years ago

951bf0fb

kim-em committed 3 years ago

1cf18028

Merge branch 'split_order_ring' into sup

kim-em committed 3 years ago

4afffd83

kim-em committed 3 years ago

d2534de6

kim-em committed 3 years ago

1ea1a32f

chore(data/int/basic): split file (#17342)

kim-em committed 3 years ago

11613e28

Merge branch 'data_nat_cast' of github.com:leanprover-community/mathlib into data_nat_cast

kim-em committed 3 years ago

8e931f78

kim-em committed 3 years ago

4293af1a

Merge remote-tracking branch 'origin/master' into data_nat_cast

kim-em committed 3 years ago

2adcae01

Merge remote-tracking branch 'origin/master' into data_nat_cast

fpvandoorn committed 3 years ago

a0534aae

chore(measure_theory/measure/finite_measure_weak_convergence): Split one file to three. (#17332)

kkytola committed 3 years ago

96e43cce

refactor(algebra/group_power/lemmas): assume `n ≠ 0` instead of `0 < n` (#17323)

urkud committed 3 years ago

03fda911

feat(geometry/manifold/*): "composition" of `charted_space` and `has_groupoid` instances (#17305)

hrmacbeth committed 3 years ago

688effb8

doc(analysis/locally_convex/with_seminorms): fix hyperlink and add first countable (#17303)

mcdoll committed 3 years ago

e4515446

doc(data/set/basic): add pointer to iff versions (#17300)

kmill committed 3 years ago

58b7f910

chore(data/list/count): use + 1 instead of nat.succ (#17161)

urkud committed 3 years ago

8b889832

feat(category_theory/groupoid/*): `is_thin` and `is_totally_disconnected` (#17122)

bottine committed 3 years ago

f187f107

feat(algebra/gcd_monoid/div): add finset.int.gcd_is_unit_of_div_gcd and similar results (#16838)

riccardobrasca committed 3 years ago

bf3b618e

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology (#16053)

ADedecker committed 3 years ago

b916d59f

feat(data/finset/basic): add lemmas about filter and (co)disjoint (#17296)

eric-wieser committed 3 years ago

7951ed37

Update src/data/pnat/basic.lean

PatrickMassot committed 3 years ago

Verified ef55dca8

fix downstream imports

kim-em committed 3 years ago

3b52a464

kim-em committed 3 years ago

d71778d2

kim-em committed 3 years ago

b5c14a8c

kim-em committed 3 years ago

99650633

kim-em committed 3 years ago

3b5700cf

Merge branch 'order_field_power' into sup

kim-em committed 3 years ago

4f377110

Merge branch 'split_data_int_basic' into sup

kim-em committed 3 years ago

1e7f0693

Newer Older