leanprover-community/mathlib

Pull Requests Commits

refactor(data/matrix/basic): make matrix a structure

eric-wieser committed 2 years ago

6a1a9f89

feat(algebra/monoid_algebra): add division by a generator (#15905)

eric-wieser committed 2 years ago

57e09a12

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

github-actions[bot] committed 2 years ago

c085f304

chore(analysis/calculus/cont_diff): split into two files (#18627)

sgouezel committed 2 years ago

dd6388c4

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

github-actions[bot] committed 2 years ago

aa3a4205

feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592)

sgouezel committed 2 years ago

4601791e

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

github-actions[bot] committed 2 years ago

290a7ba0

feat(data/matrix/kronecker): lemmas about trace, det, and inv (#18610)

eric-wieser committed 2 years ago

40cc79df

refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565)

eric-wieser committed 2 years ago

9abfa6f0

feat(number_theory/pell): group structure (#18568)

MichaelStollBayreuth committed 2 years ago

7ec29468

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)

github-actions[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)

github-actions[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

Older