leanprover-community/mathlib

Pull Requests Commits

feat(data/sum/basic): add some missing lemmas (#18184)

urkud committed 3 years ago

f4ecb599

chore(*): remove after the fact attribute [irreducible] at several places (2) (#18180)

sgouezel committed 3 years ago

39afa0b3

chore(*): remove after the fact `attribute [irreducible]` at several places (#18168)

sgouezel committed 3 years ago

565eb991

feat(ring_theory/ring_invo): add ring_invo_class (#18175)

LukasMias committed 3 years ago

ec2dfcae

chore(*): add mathlib4 synchronization comments (#18139)

github-actions[bot] committed 3 years ago

f2f413b9

chore(*): sync `list.replicate` with Mathlib 4 (#18181)

urkud committed 3 years ago

47adfab3

feat(number_theory/divisors): add `nat.cons_self_proper_divisors` (#18176)

urkud committed 3 years ago

b13c1a07

feat(linear_algebra/basis): add basis.ext_elem_iff (#18155)

xroblot committed 3 years ago

f15389d9

refactor(*): define `list.replicate` and migrate to it (#18127)

urkud committed 3 years ago

f694c7de

feat(ring_theory/valuation/valuation_subring): Add `valuation_subring.inertia_subgroup` (#17086)

mkaratarakis committed 3 years ago

88b76e4c

feat(number_theory/diophantine_approximation): add new file proving Dirichlet's approximation theorem (#18019)

MichaelStollBayreuth committed 3 years ago

dc0f25ac

feat(algebra, linear_algebra): unique instances over the trivial ring (#18160)

alreadydone committed 3 years ago

dc17b6ac

feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117)

alreadydone committed 3 years ago

0a6c26ee

chore(archive/100-theorems-list/30_ballot_problem): golf (#18126)

urkud committed 3 years ago

761f9170

feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings (#18147)

Paul-Lez committed 3 years ago

7a030ab8

chore(algebra/order/ring/canonical): use implicit variables (#18167)

riccardobrasca committed 3 years ago

a1b35592

fix(algebra/order/to_interval_mod): align `to_Ico_div` with regular division (#18105)

eric-wieser committed 3 years ago

a0ed43b3

chore(ring_theory/is_tensor_product): golf a slow proof (#18169)

eric-wieser committed 3 years ago

c4926d76

refactor(*): use `option.map₂` (#18081)

urkud committed 3 years ago

995b47e5

feat(analysis/normed/group/seminorm): add nonarchimedean (semi)norms (#17851)

mariainesdff committed 3 years ago

23c61a3c

chore(data/multiset/sort): make multiset repr a meta instance (#18163)

ChrisHughes24 committed 3 years ago

00638177

feat(data/part): add 2 lemmas (#18153)

urkud committed 3 years ago

80c43012

feat(order/bounds/basic): add `is_greatest_univ_iff` etc (#18162)

urkud committed 3 years ago

3310acfa

feat(ring_theory): equality of ideals from locally at each maximal ideal (#18142)

Vierkantor committed 3 years ago

c3350dbc

feat(analysis/convex/intrinsic): Intrinsic interior and frontier (#18027)

datokrat committed 3 years ago

9f26ebf2

feat(number_theory/zeta_values): evaluate critical values of Riemann zeta (#17994)

loefflerd committed 3 years ago

8cce17e5

feat(data/finset/sups): Set family operations (#17947)

YaelDillies committed 3 years ago

1990ff7e

feat(algebra/smul_with_zero): `a • b ≠ 0 → a ≠ 0` (#18086)

YaelDillies committed 3 years ago

12c24b79

feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775)

YaelDillies committed 3 years ago

cf8e77c6

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

leanprover-community-bot committed 3 years ago

d7943885

Newer Older