Commits leanprover-community/mathlib3

doc(linear_algebra/std_basis): add a missing backtick (#19025)

giomasce committed 2 years ago

f8c79b0a

feat(analysis/special_functions/gamma): holomorphy of `1 / Gamma` (#19012)

loefflerd committed 2 years ago

b76e9f65

chore(analysis/special_functions/pow): move around rpow/cpow tactics (#19022)

loefflerd committed 2 years ago

4fa54b33

chore(analysis/special_functions): split up `pow.lean` (#19006)

loefflerd committed 2 years ago

0b9eaaa7

chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019)

hrmacbeth committed 2 years ago

24e0c854

chore(measure_theory/measure/haar_lebesgue): remove unecessary parens (#19017)

eric-wieser committed 2 years ago

1fd85189

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

github-actions[bot] committed 2 years ago

dbdf71ce

chore(analysis/normed_space/pi_Lp): add `pi_Lp.continuous_linear_equiv` (#19014)

eric-wieser committed 2 years ago

e9f2a838

chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped` (#18873)

eric-wieser committed 2 years ago

4b884eff

feat(number_theory/legendre_symbol/*): add some API for the Legendre and the Jacobi symbol (#19011)

MichaelStollBayreuth committed 2 years ago

74a27133

chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015)

hrmacbeth committed 2 years ago

bf6a0135

fix(data/mv_polynomial): add missing `decidable_eq` arguments to lemmas (#18848)

eric-wieser committed 2 years ago

2f5b500a

doc(number_theory/pell): fix links in module docstring (#19010)

MichaelStollBayreuth committed 2 years ago

7ad820c4

chore(analysis/special_functions/gamma): split into 3 files (#19004)

loefflerd committed 2 years ago

79827670

chore(analysis/calculus/fderiv): split huge file into many pieces (#18995)

jcommelin committed 2 years ago

e3fb8404

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

github-actions[bot] committed 2 years ago

6cf59007

chore(category_theory/sites/dense_subsite): minor refactor (#19002)

kbuzzard committed 2 years ago

1d650c2e

chore(analysis/calculus/fderiv): move large file to dedicated subfolder, prepare for split (#19007)

jcommelin committed 2 years ago

58537299

feat(algebra/category/Module/change_of_rings): extension and restriction of scalars are adjoint (#15564)

jjaassoonn committed 2 years ago

403190b5

doc(algebra/euclidean_domain/defs): correct typos in doc (#19001)

faenuccio committed 2 years ago

ee7b9f9a

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

github-actions[bot] committed 2 years ago

bd15ff41

chore(measure_theory/measure/outer_measure): lemmas about zero and top (#18983)

eric-wieser committed 2 years ago

343e8020

feat(ring_theory/polynomial): show gaussian form of `hermite n` (#18896)

jakelev committed 2 years ago

066ecdb4

feat(analysis/mellin_transform): Mellin transforms (#18822)

loefflerd committed 2 years ago

9e6d4aec

chore(algebra/order/group/defs): remove some instances that cause timeouts with etaExperiment (#18985)

kim-em committed 2 years ago

b599f4e4

feat(topology/sets/compacts): add `positive_compacts.map` (#18872)

eric-wieser committed 2 years ago

8c1b484d

chore(probability/independence): create independence folder, split old file into two parts (#18987)

RemyDegenne committed 2 years ago

2f834701

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

github-actions[bot] committed 2 years ago

781cb2ee

feat(analysis/normed/order/lattice): add has_solid_norm (#18554)

xroblot committed 2 years ago

5dc275ec

chore(topology/instances/ennreal): missing smul lemmas (#18980)

eric-wieser committed 2 years ago

ec4b2eeb