leanprover-community/mathlib

Pull Requests Commits

Separate result

vihdzp committed 3 years ago

f69d2a88

vihdzp committed 3 years ago

24c4d7de

sgouezel committed 3 years ago

757891bb

feat(algebra/star/basic + analysis/normed_space/star/basic): add two eq_zero/ne_zero lemmas (#12412)

adomani committed 3 years ago

16d48d7e

feat(algebra/homology/homotopy): compatibilities of null_homotopic_map with composition and additive functors (#12392)

joelriou committed 3 years ago

3fa09c27

feat(ring_theory/polynomial/eisenstein): add mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at (#12371)

riccardobrasca committed 3 years ago

0da2d1d9

feat(algebra/algebra/subalgebra): add a helper to promote submodules to subalgebras (#12368)

eric-wieser committed 3 years ago

b0cf3d73

feat(algebra/order/monoid_lemmas_zero_lt): more lemmas using `pos_mul` and friends (#12355)

adomani committed 3 years ago

ba998da9

feat(simplex_category): various epi/mono lemmas (#11924)

joelriou committed 3 years ago

5159a8fb

feat(dynamics/fixed_points/basic): Fixed points are a subset of the range (#12423)

vihdzp committed 3 years ago

f41897d9

feat(data/nat/fib): sum of initial fragment of the Fibonacci sequence is one less than a Fibonacci number (#12416)

meithecatte committed 3 years ago

4edf36d1

refactor(measure_theory): enable dot notation for measure.map (#12350)

rish987 committed 3 years ago

59bf4540

fix(number_theory/number_field): make ring_of_integers_algebra not an instance (#12331)

ericrbg committed 3 years ago

c5045853

feat(category_theory/preadditive): the category of additive functors (#12330)

TwoFX committed 3 years ago

0ac3f9d2

feat(set_theory/ordinal): `enum` is injective (#12319)

vihdzp committed 3 years ago

691722a6

feat(topology/metric_space/pi_nat): metric structure on product spaces (#12220)

sgouezel committed 3 years ago

18f53db5

feat(ring_theory/dedekind_domain): strengthen `exist_integer_multiples` (#12184)

Vierkantor committed 3 years ago

8053f56d

feat(ring_theory/ideal): `(I : ideal R) • (⊤ : submodule R M)` (#12178)

Vierkantor committed 3 years ago

4dec7b50

feat(number_theory): padic.complete_space instance (#12424)

PatrickMassot committed 3 years ago

26d9d38f

docs(set_theory/cofinality): Fix cofinality definition (#12421)

vihdzp committed 3 years ago

bf203b95

feat(data/complex/basic): add abs_hom (#12409)

ericrbg committed 3 years ago

02cad2cd

chore(algebra/group/hom): more generic `f x ≠ 1` lemmas (#12404)

Vierkantor committed 3 years ago

bc35902c

feat(algebra/algebra/spectrum): show the star and spectrum operations commute (#12351)

j-loreaux committed 3 years ago

ca0ff3ad

feat(set_theory/cofinality): Prove simple theorems on regular cardinals (#12328)

vihdzp committed 3 years ago

f7a6fe9e

chore(analysis/normed_space/star/basic): golf a proof (#12420)

adomani committed 3 years ago

16ad25c2

feat(data/list/destutter): add `list.destutter` to remove chained duplicates (#11934)

ericrbg committed 3 years ago

228ab96a

use has_succ_of_is_limit

sgouezel committed 3 years ago

b1fe3a49

Apply suggestions from code review

sgouezel committed 3 years ago

Verified 43bb06b6

feat(data/part): Lemmas for get on binary function instances (#12194)

BoltonBailey committed 3 years ago

46b9d057

sgouezel committed 3 years ago

d68ee034

Older