leanprover-community/mathlib

Pull Requests Commits

refactor(category_theory/monoidal): rearrange simp lemmas to work better with coherence (#13409)

kim-em committed 3 years ago

85075bcc

feat(analysis/convex/measure): a convex set is null-measurable (#13138)

urkud committed 3 years ago

9f75d75a

feat(data/nat/choose): add facts about the multiplicity of primes in the factorisation of central binomial coefficients (#9925)

Smaug123 committed 3 years ago

2c15ce14

feat(data/set/prod): add `set.eval_image_pi_subset` (#13613)

urkud committed 3 years ago

2825f353

chore(data/finsupp/fin): golf some proofs (#13607)

Ruben-VandeVelde committed 3 years ago

14b0e32b

feat(algebra/periodic): add lemmas `periodic.prod`, `periodic.smul`, `antiperiodic.smul` (#13496)

ocfnash committed 3 years ago

b7538a30

feat(set_theory/game/pgame): remove nolint (#13680)

vihdzp committed 3 years ago

4bfae3d8

feat(dynamics/periodic_pts): `pow_smul_eq_iff_minimal_period_dvd` (#13676)

tb65536 committed 3 years ago

9e8d1075

feat(topology/algebra): actions on the opposite type are continuous (#13671)

eric-wieser committed 3 years ago

7231172e

feat(ring_theory/witt_vector/frobenius): add `witt_vector.frobenius_equiv` (#13666)

eric-wieser committed 3 years ago

ed10ba23

feat(data/zmod/basic): `-1 : zmod n` lifts to `n - 1` (#13665)

tb65536 committed 3 years ago

6d3ca07a

feat(dynamics/periodic_pts): Iteration is injective below the period (#13660)

tb65536 committed 3 years ago

ad0a3e66

feat(analysis/complex/roots_of_unity): arg of a primitive root (#13583)

ericrbg committed 3 years ago

6710d655

feat(algebra/order/hom/ring): There's at most one hom between linear ordered fields (#13601)

YaelDillies committed 3 years ago

b35ed400

feat(number_theory/legendre_symbol/quadratic_reciprocity): Alternate forms of `exists_sq_eq_neg_one` (#13594)

vihdzp committed 3 years ago

d795ea4b

feat(logic/basic): `congr_fun` for heterogeneous equality (#13591)

vihdzp committed 3 years ago

e251ef77

feat(algebra/big_operators/basic): mk0_prod (#13582)

ericrbg committed 3 years ago

e059fdf9

feat(special_functions/gamma): recurrence relation for Gamma function (#13156)

loefflerd committed 3 years ago

f02c7844

feat(group_theory/subgroup/basic): Cyclic subgroups are commutative (#13663)

tb65536 committed 3 years ago

ef3769db

feat(order/filter): add `filter.coprod_bot` etc (#13662)

urkud committed 3 years ago

b0fe3cd2

feat(group_theory/group_action/basic): More API for `quotient_action` (#13661)

tb65536 committed 3 years ago

feb9aed4

refactor(analysis/convex/basic): rewrite a few proofs (#13658)

urkud committed 3 years ago

46563c5c

chore(analysis/convex/topology): generalize a few lemmas (#13656)

urkud committed 3 years ago

7d64215f

chore(number_theory/padics/*): tidy some proofs (#13652)

Ruben-VandeVelde committed 3 years ago

c24f1f2b

chore(field_theory/finite/polynomial): tidy + remove nolints (#13645)

ericrbg committed 3 years ago

962bfcdb

chore(ring_theory/witt_vector/isocrystal): speed up the proof (#13644)

yuma-mizuno committed 3 years ago

b6a4be44

feat(topology/algebra/matrix): `matrix.block_diagonal` is continuous (#13641)

eric-wieser committed 3 years ago

9c861e32

feat(group_theory/complement): The range of a section `G ⧸ H → G` is a transversal (#13623)

tb65536 committed 3 years ago

b1b2cab4

refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#13622)

tb65536 committed 3 years ago

6cbf986a

refactor(linear_algebra/quotient): Use the same quotient relation as add_subgroup (#13620)

eric-wieser committed 3 years ago

b6c8c0d4

Newer Older