leanprover-community/mathlib3

Pull Requests Commits

stuart-presnell committed 3 years ago

21dd4e3f

Revert "Restore original `data/nat/multiplicity`"

stuart-presnell committed 3 years ago

b4664910

Restore original `data/nat/multiplicity`

stuart-presnell committed 3 years ago

bd7cb5d4

Format brackets

stuart-presnell committed 3 years ago

559f0a19

Delete comments

stuart-presnell committed 3 years ago

d8eb84fd

Move `factorization_choose` lemmas

stuart-presnell committed 3 years ago

4ca4d701

Add section headers

stuart-presnell committed 3 years ago

2cc88b8b

Remove `factorization_pow_self`

stuart-presnell committed 3 years ago

bdc5ffe9

Move vars into lemma statements

stuart-presnell committed 3 years ago

f0b0e699

Cut comments and `multiplicity` versions

stuart-presnell committed 3 years ago

0ae46034

Move material to new file `factorial/factorization`

stuart-presnell committed 3 years ago

e02abdcc

stuart-presnell committed 3 years ago

f9d3b5ca

Remove commented material

stuart-presnell committed 3 years ago

d4807207

Make `Icc_insert_succ` a simp lemma

stuart-presnell committed 3 years ago

a12ebf49

Delete lines commented in merge

stuart-presnell committed 3 years ago

0a276d03

Delete lemmas PRed elsewhere

stuart-presnell committed 3 years ago

f8ba7ff2

Merge branch 'master' into SP_multiplicity_nat_rewrite

stuart-presnell committed 3 years ago

5f0b4c0e

refactor(data/int/cast): Use hom classes (#16024)

YaelDillies committed 3 years ago

972aa423

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

leanprover-community-bot committed 3 years ago

b46c8953

chore(algebra/big_operators/pi): rename `w` to `H` in assumptions (#16166)

urkud committed 3 years ago

ec73f6e3

feat(group_theory/coset): Right cosets are orbits (#16119)

tb65536 committed 3 years ago

aac3141e

feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118)

tb65536 committed 3 years ago

eaeb4583

feat(algebraic_topology): split simplicial objects (#16072)

joelriou committed 3 years ago

df967907

feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147)

alreadydone committed 3 years ago

ee261437

refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)

YaelDillies committed 3 years ago

67488dff

chore(field_theory/*): Fix lint (#16149)

YaelDillies committed 3 years ago

c2c31b52

feat(data/finset/pointwise): `-s • t = -(s • t)` (#16138)

YaelDillies committed 3 years ago

4a0f332e

split(analysis/convex/segment): Split off `analysis/convex.basic` (#16112)

YaelDillies committed 3 years ago

4705dd0d

feat(ring_theory/polynomial): Vieta's formula in terms of `polynomial.roots` (#14908)

alreadydone committed 3 years ago

8fdec909

feat(algebra/star/star_alg_hom): define unital and non-unital `star_alg_hom`s (#16089)

j-loreaux committed 3 years ago

09d7fe37

Older