leanprover-community/mathlib

Pull Requests Commits

j-loreaux committed 2 years ago

9dbfabaf

j-loreaux committed 2 years ago

506535c1

j-loreaux committed 2 years ago

1a24ecf3

fix type class inference loop

j-loreaux committed 2 years ago

759b0997

j-loreaux committed 2 years ago

47a1df5e

add non-unital star subalgebras

j-loreaux committed 2 years ago

0444256b

finish up non_unital_subring

j-loreaux committed 2 years ago

e3fea45e

improve non-unital subring

j-loreaux committed 2 years ago

b75e3b9f

remove bit on actions

j-loreaux committed 2 years ago

4bd54a19

j-loreaux committed 2 years ago

b76c4c59

Merge branch 'master' into j-loreaux/cfc-playground

j-loreaux committed 2 years ago

4ab67647

many changes and additions

j-loreaux committed 2 years ago

84f943c2

chore(data/set/intervals/monotone): fix names (#18924)

urkud committed 2 years ago

4d06b17a

chore(analysis/normed_space/basic): rename `abs_norm_eq_norm` to `abs_norm` (#18921)

urkud committed 2 years ago

f9dd3204

chore(data/{complex,is_R_or_C}/basic): fix name of `eq_conj_iff_*` lemmas (#18922)

eric-wieser committed 2 years ago

caa58cbf

feat(probability/kernel/composition): add a notation for the product of kernels (#18918)

RemyDegenne committed 2 years ago

15e02bcd

chore(ring_theory/polynomial/quotient): remove spurious restrict_scalars (#18916)

kim-em committed 2 years ago

61d8b824

refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` (#18912)

eric-wieser committed 2 years ago

645b6de4

feat(data/mv_polynomial/basic): add and generalize some lemmas from finsupp and monoid_algebra (#18855)

Hagb committed 2 years ago

f69db8ce

feat(analysis/special_functions): file for evaluations of specific improper integrals (#18821)

loefflerd committed 2 years ago

ec452806

feat(data/list/cycle): well-founded or transitive irreflexive relations don't have cycles (#18512)

vihdzp committed 2 years ago

7413128c

feat(algebra/algebra/basic): add shortcut instance (#18907)

Ruben-VandeVelde committed 2 years ago

36b8aa61

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

leanprover-community-bot committed 2 years ago

ef553359

feat(measure_theory/constructions/polish): a Polish Borel space is measurably equivalent to a subset of the reals (#18881)

Felix-Weilacher committed 2 years ago

11d5ff21

chore(analysis/special_functions): Reduce imports in special_functions (#18909)

loefflerd committed 2 years ago

2c1d8ca2

chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911)

kim-em committed 2 years ago

33085c97

refactor(category_theory): removing additive_category (#18903)

joelriou committed 2 years ago

362c2263

refactor(number_theory/modular_forms/slash_actions): use the same notation everywhere (#18886)

eric-wieser committed 2 years ago

ef74e2bd

feat(ring_theory/norm): add norm_norm (#18860)

xroblot committed 2 years ago

fecd3520

feat(analysis/convex/cone/proper): define closure of a convex cone (#16335)

apurvnakade committed 2 years ago

620ba06c

Older