leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 3 years ago

4817e288

add lemma + golf

vihdzp committed 3 years ago

b0db584f

Update limit.lean

vihdzp committed 3 years ago

7d7d1cf1

vihdzp committed 3 years ago

3463e311

instance → def

vihdzp committed 3 years ago

3569db85

Update limit.lean

vihdzp committed 3 years ago

e664113b

Merge branch 'master' into is_succ_limit_pred'

vihdzp committed 3 years ago

07f6719a

docs(undergrad): add pointwise convergence (#15601)

PatrickMassot committed 3 years ago

e27e99b9

docs(undergrad): clean up distribution section (#15600)

PatrickMassot committed 3 years ago

2f99fd41

docs(undergrad): add polar integration (#15597)

PatrickMassot committed 3 years ago

d96fc102

refactor(data/list/chain): `transitive` → `is_trans` on `chain.pairwise` (#15571)

vihdzp committed 3 years ago

c97887bd

feat(analysis/calculus/cont_diff): generalize `mul` lemmas to a normed algebra (#15595)

urkud committed 3 years ago

d98479aa

doc(number_theory/bernoulli_polynomials): a few small improvements (#15599)

alexjbest committed 3 years ago

91416440

feat(order/succ_pred/limit): Successor and predecessor limits (#15001)

vihdzp committed 3 years ago

767aeb39

feat(order/initial_seg): Initial/principal segment from empty type (#15375)

vihdzp committed 3 years ago

9bf23b0a

feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575)

eric-wieser committed 3 years ago

d749b205

feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

mcdoll committed 3 years ago

c0c910de

chore(data/real/basic,number_theory/padics/padic_numbers): eliminate `real.of_rat` and `padic.of_rat` (#15569)

eric-wieser committed 3 years ago

591992d7

feat(topology/partition_of_unity): local to global (#15490)

urkud committed 3 years ago

7f16dd20

refactor(set_theory/zfc): make `Class` morally `Set → Prop` (#15248)

vihdzp committed 3 years ago

f05fdcac

feat(set_theory/cardinal/ordinal): basic properties on Beth numbers (#14989)

vihdzp committed 3 years ago

99625b1b

feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044)

joelriou committed 3 years ago

d29aca84

doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)

eric-wieser committed 3 years ago

72e0e9a5

feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#15548)

vihdzp committed 3 years ago

8672734e

fix(data/set_like): `coe_sort_trans` should have low priority (#15489)

Vierkantor committed 3 years ago

8983bec7

refactor(field_theory/*): Refactor `normal` to use `is_algebraic` (#15421)

tb65536 committed 3 years ago

62b5bb74

feat(linear_algebra/projective_space/subspace): defines subspaces of a projective space (#15391)

Michael14071407 committed 3 years ago

90a44f6b

feat(ring_theory/graded_algebra/basic): add lemma `proj_homogeneous_mul` (#15264)

jjaassoonn committed 3 years ago

976f5106

feat(topology/basic): a condition implying that a sequence of functions locally stabilizes (#15580)

urkud committed 3 years ago

4a09c733

feat(logic/nonempty): `pi.nonempty` instance (#15574)

vihdzp committed 3 years ago

6b5a1730

Older