Commits leanprover-community/mathlib

chore(data/{nat,int}/cast/field): generalize to division_ring (#18598)

eric-wieser committed 3 years ago

acee671f

feat(number_theory/modular_forms): Jacobi theta function (#18564)

loefflerd committed 3 years ago

34d37973

feat(analysis/inner_product_space/projection): express `orthogonal_projection` using `linear_proj_of_is_compl` (#18243)

ADedecker committed 3 years ago

22f57723

chore(algebra/order/nonneg/*): Separate `floor_ring` from `field` (#18596)

YaelDillies committed 3 years ago

b3f4f007

chore(algebra/order/field/basic): Rename `pow_minus_two_nonneg` (#18591)

YaelDillies committed 3 years ago

acb3d204

refactor(geometry/euclidean): split out spheres (#18220)

jsm28 committed 3 years ago

eea141bc

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

kim-em committed 3 years ago

5120cf49

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

kex-y committed 3 years ago

97d1aa95

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

eric-wieser committed 3 years ago

ce7e9d53

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

eric-wieser committed 3 years ago

a3786508

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

urkud committed 3 years ago

83f81aea

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

YaelDillies committed 3 years ago

992efbda

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

eric-wieser committed 3 years ago

29d5700b

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

eric-wieser committed 3 years ago

01118344

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

github-actions[bot] committed 3 years ago

10bf4f82

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

eric-wieser committed 3 years ago

4681620d

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

astrainfinita committed 3 years ago

1a313d8b

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

eric-wieser committed 3 years ago

3fc0b254

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

eric-wieser committed 3 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 3 years ago

ceb887dd

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

eric-wieser committed 3 years ago

2fd0de23

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

eric-wieser committed 3 years ago

bd1fc183

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

MichaelStollBayreuth committed 3 years ago

2196ab36

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

github-actions[bot] committed 3 years ago

69c6a5a1

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

eric-wieser committed 3 years ago

795b5018

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

eric-wieser committed 3 years ago

1e320130

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

eric-wieser committed 3 years ago

2af08364

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

ericrbg committed 3 years ago

c985ae98

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

eric-wieser committed 3 years ago

f24cc289

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

jcommelin committed 3 years ago

da420a8c