leanprover-community/mathlib

Pull Requests Commits
feat(analysis/seminorm): add add_group_seminorm (#14336)
mariainesdff committed 3 years ago
cff439d8
feat(number_theory): define ramification index and inertia degree (#14332)
Vierkantor committed 3 years ago
585a1bf3
feat(data/sigma,data/ulift,logic/equiv): add missing lemmas (#14903)
urkud committed 3 years ago
cc4b8e55
chore(number_theory/lucas_lehmer): remove `has_to_pexpr` instances (#14905)
eric-wieser committed 3 years ago
cf231995
chore(ring_theory/polynomial/symmetric): golf proofs (#14866)
eric-wieser committed 3 years ago
416edbd3
fix(meta/expr): remove `has_reflect.has_to_pexpr` (#14901)
eric-wieser committed 3 years ago
c45e5d58
chore(analysis/special_functions/log/basic): golf a proof (#14898)
urkud committed 3 years ago
2a732ed5
feat(order/filter/basic): add some lemmas about `eventually_le` (#14891)
kex-y committed 3 years ago
23918a54
refactor(data/set/countable): make `set.countable` protected (#14886)
urkud committed 3 years ago
12e5f2e0
refactor(data/finite/card): split from `basic` (#14885)
urkud committed 3 years ago
d8fc588d
feat(topology/basic): `sum.elim` of locally finite set families is locally finite (#14826)
urkud committed 3 years ago
c2719adf
feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824)
YaelDillies committed 3 years ago
44bb35e5
chore(data/rat): rename `data.rat.basic` to `data.rat.defs` (#14895)
Vierkantor committed 3 years ago
38642efc
chore(algebra/{group_power,order}): split off field lemmas (#14849)
Vierkantor committed 3 years ago
f57c0cdc
a test with forall, exists
adomani committed 3 years ago
dabbbab4
cosmetic
adomani committed 3 years ago
c5ca2bc9
cleared up
adomani committed 3 years ago
8d97f9d8
Merge branch 'master' into aa_sort
adomani committed 3 years ago
3fb5f3bb
feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541)
fpvandoorn committed 3 years ago
d939b0e6
feat(set_theory/surreal/basic): define map `surreal →+o game` (#14783)
vihdzp committed 3 years ago
ad497685
Merge branch 'master' into aa_sort
adomani committed 3 years ago
318e16a3
feat(combinatorics/simple_graph/connectivity): Connectivity is a graph property (#14865)
YaelDillies committed 3 years ago
61b837fb
fix(tactic/apply_fun.lean): instantiate mvars in apply_fun (#14882)
digama0 committed 3 years ago
f3cd150b
chore(linear_algebra/alternating): more lemmas about `curry_left` (#14844)
eric-wieser committed 3 years ago
3b6552e0
feat(data/finsupp/basic): make `prod_add_index_of_disjoint` to_additive (#14786)
stuart-presnell committed 3 years ago
d9537732
feat(data/sigma): add reflected instance (#14764)
eric-wieser committed 3 years ago
3e66afe7
feat(order/conditionally_complete_lattice): add `cInf_le_cInf'` (#14719)
user7230724 committed 3 years ago
b779513a
golf(data/polynomial): factorization into linear factors when #roots=degree (#14862)
alreadydone committed 3 years ago
2d70b946
feat(topology/metric_space/basic): Add `ball_comm` lemmas (#14858)
linesthatinterlace committed 3 years ago
ee123628
doc(data/polynomial/div): fix runaway code block (#14864)
eric-wieser committed 3 years ago
2b5a5770
Terms Of Use Privacy Policy Refund Policy Impressum