leanprover-community/mathlib3

Pull Requests Commits

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

feat(data/nat/prime): nat.prime.eq_pow_iff (#8917)

tb65536 committed 4 years ago

9df3f0d4

feat(linear_algebra/matrix/symmetric): add a file (#8955)

l534zhan committed 4 years ago

a4df4609

feat(data/nat/choose/dvd): generalize to division rings (#8997)

jcommelin committed 4 years ago

18d7b743

feat(ring_theory/ideal/operations): ideal.pow_mem_pow (#8996)

jcommelin committed 4 years ago

4435e909

feat(order/prime_ideal, order/boolean_algebra): small lemmas about prime ideals (#8980)

atarnoam committed 4 years ago

dcc45b42

feat(ring_theory/ideal/operations): ring_hom.ker_is_maximal_of_surjective (#8990)

jcommelin committed 4 years ago

7f7f3d90

feat(linear_algebra/prod): lemmas about ker and range (#8989)

ChrisHughes24 committed 4 years ago

9d86dad0

feat(linear_algebra/basic): galois insertion lemmas for map and comap (#8978)

ChrisHughes24 committed 4 years ago

855613ee

feat(category_theory/basic/category): Combine and improve API on preorder categories. (#8982)

justus-springer committed 4 years ago

b57af8a5

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

leanprover-community-bot committed 4 years ago

b9d8081e

chore(group_theory/group_action/defs): weaken assumptions of `mul_smul_comm` and `smul_mul_assoc` (#8972)

eric-wieser committed 4 years ago

464c3d73

docs(topology/algebra/floor_ring): add module docstring (#8969)

YaelDillies committed 4 years ago

6ab66958

fix(data/setoid/partition): make def more readable (#8951)

kbuzzard committed 4 years ago

66cb5e07

feat(ring_theory/subring): field structure on centers of a division_ring (#8472)

shingtaklam1324 committed 4 years ago

93a15d6b

feat(algebra/order_functions): (min|max)_eq_iff (#8911)

pechersky committed 4 years ago

3a0dddcc

docs(data/subtype): add module docstring (#8900)

YaelDillies committed 4 years ago

39cea43a

chore(algebra/divisibility): help dot notation on `dvd` (#8766)

YaelDillies committed 4 years ago

710a76e7

feat(analysis/complex/basic): convex_on.sup (#8958)

pechersky committed 4 years ago

5e27f509

feat(algebra/ordered_ring): `linear_ordered_semiring` extends `linear_ordered_add_comm_monoid` (#8961)

pechersky committed 4 years ago

fdc24f53

feat(group_theory/group_action/basic): class formula, Burnside's lemma (#8801)

ADedecker committed 4 years ago

d821860f

feat(number_theory): define number fields, function fields and their rings of integers (#8701)

Vierkantor committed 4 years ago

17747c09

feat(ring_theory/ideal): generalize from `integral_closure` to `is_integral_closure` (#8944)

Vierkantor committed 4 years ago

88525a98

feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957)

tb65536 committed 4 years ago

55a7d385

Newer Older