leanprover-community/mathlib

Pull Requests Commits

feat(data/multiset/basic): Add a result on intersection of multiset with `repeat a n` (#9038)

Paul-Lez committed 4 years ago

bfcf73fa

feat(field_theory/algebraic_closure): polynomials in an algebraically closed fields have roots (#9037)

ChrisHughes24 committed 4 years ago

3148cfe1

chore(data/nat/mul_ind): make docgen happy (#9036)

ericrbg committed 4 years ago

3a624194

feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034)

Vierkantor committed 4 years ago

11284f2f

feat(set/lattice): two lemmas about when sInter is empty (#9033)

atarnoam committed 4 years ago

86dd706c

chore(set_theory/pgame): add protected (#9022)

apurvnakade committed 4 years ago

98cbad7b

feat(measure_theory/measure/vector_measure): zero is absolutely continuous wrt any vector measure (#9007)

kex-y committed 4 years ago

c83c22dc

feat(linear_algebra/affine_space/independent): affine independence is preserved by affine maps (#9005)

ocfnash committed 4 years ago

339c2c35

feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s (#9026)

Vierkantor committed 4 years ago

c2e6e62a

feat(algebra/pointwise): enable pointwise add_action (#9017)

alexjbest committed 4 years ago

448f821d

feat(linear_algebra/basic): surjective_of_iterate_surjective (#9006)

ChrisHughes24 committed 4 years ago

f0c3f9e8

feat(linear_algebra/basic): of_le_injective (#8977)

ChrisHughes24 committed 4 years ago

d16cb001

feat(data/fin): pos_iff_nonempty (#8975)

ChrisHughes24 committed 4 years ago

c0f01eed

chore(field_theory/fixed): reuse existing `mul_semiring_action.to_alg_hom` by providing `smul_comm_class` (#8965)

eric-wieser committed 4 years ago

de37a6aa

feat(topology/continuous_function/basic): add `continuous_map.Icc_extend` (#8952)

shingtaklam1324 committed 4 years ago

2aebabca

feat(algebra/module/ordered): redefine `ordered_module` as `ordered_smul` (#8930)

pechersky committed 4 years ago

773b45f7

refactor(group_theory/*): Move Cauchy's theorem (#8916)

tb65536 committed 4 years ago

e8fff266

feat(group_theory/submonoid/membership): add log, exp lemmas (#8870)

apurvnakade committed 4 years ago

893c4746

feat(algebra/lattice_ordered_group): add basic theory of lattice ordered groups (#8673)

mans0954 committed 4 years ago

74373b81

feat(data/polynomial/eval): leval, eval as linear map (#8999)

jcommelin committed 4 years ago

c5636921

lint(tactic/*): break long lines (#8973)

YaelDillies committed 4 years ago

1f103908

refactor(*): replace `function.swap` by `swap` (#8612)

fpvandoorn committed 4 years ago

1bc59c99

feat(group_theory/coset): Interaction between quotient_group.mk and right multiplication by elements of the subgroup (#8970)

tb65536 committed 4 years ago

a3997288

feat(data/nat/choose/vandermonde): Vandermonde's identity for binomial coefficients (#8992)

jcommelin committed 4 years ago

0a94b29f

chore(scripts): update nolints.txt (#9014)

leanprover-community-bot committed 4 years ago

9fc45d81

fix(algebra/ordered_monoid): slay with_top monoid diamonds caused by irreducibility (#8926)

pechersky committed 4 years ago

2ea1650d

feat(linear_algebra/pi): pi_option_equiv_prod (#9003)

ChrisHughes24 committed 4 years ago

fd0cdaee

feat(data/equiv/fin): fin_sum_fin_equiv simp lemmas (#9001)

ChrisHughes24 committed 4 years ago

8ff139a0

feat(algebra): define "Euclidean" absolute values (#8949)

Vierkantor committed 4 years ago

7729bb6d

feat(set_theory/cardinal): cardinal.to_nat_mul (#8943)

tb65536 committed 4 years ago

28592d99

Newer Older