leanprover-community/mathlib

Pull Requests Commits

urkud committed 2 years ago

77800279

Merge branch 'master' into YK-stream-struct

urkud committed 2 years ago

a741c47c

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

xroblot committed 2 years ago

f15389d9

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

urkud committed 2 years ago

f694c7de

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

mkaratarakis committed 2 years ago

88b76e4c

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

MichaelStollBayreuth committed 2 years ago

dc0f25ac

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

alreadydone committed 2 years ago

dc17b6ac

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

alreadydone committed 2 years ago

0a6c26ee

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

urkud committed 2 years ago

761f9170

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

Paul-Lez committed 2 years ago

7a030ab8

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

riccardobrasca committed 2 years ago

a1b35592

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

eric-wieser committed 2 years ago

a0ed43b3

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

eric-wieser committed 2 years ago

c4926d76

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

urkud committed 2 years ago

995b47e5

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

mariainesdff committed 2 years ago

23c61a3c

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

ChrisHughes24 committed 2 years ago

00638177

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

urkud committed 2 years ago

80c43012

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

urkud committed 2 years ago

3310acfa

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

Vierkantor committed 2 years ago

c3350dbc

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

datokrat committed 2 years ago

9f26ebf2

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

loefflerd committed 2 years ago

8cce17e5

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

YaelDillies committed 2 years ago

1990ff7e

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

YaelDillies committed 2 years ago

12c24b79

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

YaelDillies committed 2 years ago

cf8e77c6

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

leanprover-community-bot committed 2 years ago

d7943885

feat(data/finset/basic): add a `can_lift` instance (#18152)

urkud committed 2 years ago

f6a7bd6f

chore(data/list): golf, merge 2 files (#18120)

urkud committed 2 years ago

527e406f

feat(data/multiset/basic): `multiset.coe_eq_singleton` (#15910)

vihdzp committed 2 years ago

f3187269

chore(probability_mass_function/monad): Use standard `Union` notation (#18154)

dtumad committed 2 years ago

feb165c9

fix(*): fix typo in the word subtraction (#18145)

eric-wieser committed 2 years ago

d50b12ae

Older