leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 2 years ago

b12a1f55

Merge remote-tracking branch 'origin/master' into eric-wieser/antidiagonal-with_bot

eric-wieser committed 2 years ago

d1f47a3e

chore (data/finset/sym): remove unnecessary alias (#18603)

xroblot committed 2 years ago

02ba8949

fix(analysis/inner_product_space/pi_L2): add missing type cast functions (#18574)

eric-wieser committed 2 years ago

9f0d61b4

chore(topology/basic): backport a generalization to Sort (#18544)

eric-wieser committed 2 years ago

88b8a77d

chore(data/fintype/fin): add Iio lemmas (#18600)

eric-wieser committed 2 years ago

75957565

chore(ring_theory/power_series/basic): remove commutativity assumption (#18599)

eric-wieser committed 2 years ago

2d5739b6

chore(algebra): generalize typeclass arguments from field to semifield (#18597)

YaelDillies committed 2 years ago

30413fc8

chore(algebra/ring/ulift): Split off and golf field instances (#18590)

YaelDillies committed 2 years ago

13e18cfa

feat(analysis/normed_space/quaternion_exponential): lemmas about the quaternion exponential (#18349)

eric-wieser committed 2 years ago

da3fc4a3

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

eric-wieser committed 2 years ago

acee671f

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

loefflerd committed 2 years ago

34d37973

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

ADedecker committed 2 years ago

22f57723

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

YaelDillies committed 2 years ago

b3f4f007

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

YaelDillies committed 2 years ago

acb3d204

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

jsm28 committed 2 years ago

eea141bc

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

refactor(data/list/nat_antidiagonal): extend to `enat`

eric-wieser committed 2 years ago

a4e47e76

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

eric-wieser committed 2 years ago

af8f9bc2

Older