leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 2 years ago

5fe3567b

chore(data/mv_polynomial): reverse an import (#18593)

kim-em committed 2 years ago

5120cf49

feat(probability/kernel/invariance): Define pushforward of measure along a kernel (#18244)

kex-y committed 2 years ago

97d1aa95

feat(algebra/triv_sq_zero_ext): lemmas about big operators (#18488)

eric-wieser committed 2 years ago

ce7e9d53

chore(analysis/inner_product_space/basic): add inner_self_ne_zero (#18587)

eric-wieser committed 2 years ago

a3786508

refactor(topology/algebra/open_subgroup): use `set_like` (#18585)

urkud committed 2 years ago

83f81aea

feat(analysis/normed/order/upper_lower): Thickening an upper set (#17257)

YaelDillies committed 2 years ago

992efbda

chore(geometry/manifold/instances/sphere): speedup a proof (#18586)

eric-wieser committed 2 years ago

29d5700b

chore(order/with_bot): lemmas about unbot and untop (#18582)

eric-wieser committed 2 years ago

01118344

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

github-actions[bot] committed 2 years ago

10bf4f82

fix(analysis/inner_product_space): make type families explicit for `orthogonal_family` and `is_hilbert_sum` (#18584)

eric-wieser committed 2 years ago

4681620d

feat(order/initial_seg): add lemmas about `acc` and `well_founded` (#18527)

astrainfinita committed 2 years ago

1a313d8b

chore(analysis/inner_product_space): rename `_sym` to `_symm` (#18580)

eric-wieser committed 2 years ago

3fc0b254

chore(analysis/inner_product_space/basic): make arguments explicit (#18579)

eric-wieser committed 2 years ago

af8f9bc2

feat(algebra/char_p/basic): refactor proof of add_pow_char_of_commute to extract a statement true in all rings (#11364)

alexjbest committed 2 years ago

ceb887dd

chore(analysis/normed_space/pi_Lp): missing scalar tower instances (#18577)

eric-wieser committed 2 years ago

2fd0de23

refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_like instances (#18575)

eric-wieser committed 2 years ago

bd1fc183

refactor(algebra/group/basic): rework lemmas on inv and neg (#17483)

MichaelStollBayreuth committed 2 years ago

2196ab36

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

github-actions[bot] committed 2 years ago

69c6a5a1

chore(number_theory/pell_matiyasevic): generalize `is_pell` to arbitary `d` (#18573)

eric-wieser committed 2 years ago

795b5018

feat(analysis/normed_space/*exponential): more results about `star` (#18553)

eric-wieser committed 2 years ago

1e320130

refactor(number_theory/zsqrtd): replace `zsqrtd.conj` with `star` (#18572)

eric-wieser committed 2 years ago

2af08364

chore(topology/order/basic): generalise frontier_Icc (#18571)

ericrbg committed 2 years ago

c985ae98

chore(data/finset/locally_finite): lemmas about open intervals (#18533)

eric-wieser committed 2 years ago

f24cc289

refactor(*): reduce dependencies on ring_theory.ideal.quotient_operations (#18530)

jcommelin committed 2 years ago

da420a8c

feat(probability/kernel/composition): composition of kernels (#17974)

RemyDegenne committed 2 years ago

3180fab6

feat(probability/probability_mass_function): basic lawful monad lemmas for `pmf`. (#18469)

dtumad committed 2 years ago

4ac69b29

feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680)

fpvandoorn committed 2 years ago

ddec54a7

feat(number_theory/pell): add exists_pos_of_not_is_square (#18567)

MichaelStollBayreuth committed 2 years ago

5b05c634

chore(data/matrix/basic): add a star_module instance (#18557)

eric-wieser committed 2 years ago

21e3562c

Older