leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 2 years ago

c52ea192

chore(linear_algebra/affine_space/affine_subspace) add set_like instance (#18622)

mcdoll committed 2 years ago

e96bdfbd

chore(analysis/inner_product_space/basic): explicit `𝕜` argument for `innerₛₗ` and `innerSL` (#18613)

eric-wieser committed 2 years ago

c78cad35

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

leanprover-community-bot committed 2 years ago

1dac236e

feat(algebra/group/commute): `div` lemmas (#18607)

YaelDillies committed 2 years ago

05101c3d

chore(linear_algebra/free_module/basic): golf a proof (#18615)

eric-wieser committed 2 years ago

4e7e7009

perf(group_theory/torsion): Speedup `torsion_mul_equiv` (#18614)

YaelDillies committed 2 years ago

1f4705cc

chore(topology/algebra/module/basic): move a lemma to a new file (#18608)

urkud committed 2 years ago

f430769b

chore(geometry/euclidean/sphere/basic): generalize typeclasses (#18605)

eric-wieser committed 2 years ago

027ff1e4

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

leanprover-community-bot committed 2 years ago

93287238

feat(algebra/quadratic_discriminant): generalize, use `ne_zero` (#18606)

urkud committed 2 years ago

e085d1df

feat(data/set/sups): Set family operations (#18172)

YaelDillies committed 2 years ago

20715f4a

feat(algebra/*/opposite): Missing instances (#18602)

YaelDillies committed 2 years ago

acebd8d4

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

Older