Commits leanprover-community/mathlib

chore(analysis/normed_space/star/basic): split (#18194)

hrmacbeth committed 2 years ago

3249a849

chore(analysis/normed/field/basic): split (#18195)

hrmacbeth committed 2 years ago

008205aa

feat(data/polynomial): Add Partial Fraction Decomposition (Existence) (#17709)

thefundamentaltheor3m committed 2 years ago

6e70e0d4

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

leanprover-community-bot committed 2 years ago

e04043d6

feat(number_theory/diophantine_approximation): add more results (#18193)

MichaelStollBayreuth committed 2 years ago

9956c380

feat(algebra/order/to_interval_mod): more relations between `to_Ixx_{mod/div}` definitions (#17933)

eric-wieser committed 2 years ago

a993e7ee

feat(group_theory/perm/cycle/basic): Countable sets admit cycles (#17909)

YaelDillies committed 2 years ago

18562995

feat(analysis/seminorm): characterize continuity of seminorms by closed balls (#17249)

ADedecker committed 2 years ago

c46f021f

feat(topology/algebra/equicontinuity): a family of group homomorphisms is equicontinuous iff it is equicontinuous at `1` (#17128)

ADedecker committed 2 years ago

01ad394a

fix(analysis/inner_product_space/basic): restore `bilin_form_of_real_inner` (#18093)

eric-wieser committed 2 years ago

b4f03bc5

chore(analysis/convex/exposed): downgrade imports (#18186)

hrmacbeth committed 2 years ago

48024901

feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base (#17632)

nielsvoss committed 2 years ago

c0439b48

chore(topology/metric_space/isometry): rename isometric to isometry_equiv (#18191)

JovanGerb committed 2 years ago

4b99fe0a

chore(analysis/convex/body): downgrade imports (#18185)

hrmacbeth committed 2 years ago

e6c26fe3

chore(data/list): reorder arguments of `list.nthd` (#18182)

urkud committed 2 years ago

1447cae8

feat(group_theory/perm/cycle/basic): Partition `s × s` into shifted diagonals (#17910)

YaelDillies committed 2 years ago

56ca12cc

feat(data/fin/tuple): rename `fin.append` to `matrix.vec_append`, introduce a new `fin.append` and `fin.repeat`. (#10346)

eric-wieser committed 2 years ago

91288e35

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

urkud committed 2 years ago

f4ecb599

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

sgouezel committed 2 years ago

39afa0b3

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

sgouezel committed 2 years ago

565eb991

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

LukasMias committed 2 years ago

ec2dfcae

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

leanprover-community-bot committed 2 years ago

f2f413b9

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

urkud committed 2 years ago

47adfab3

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

urkud committed 2 years ago

b13c1a07

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