leanprover-community/mathlib3

Pull Requests Commits

hrmacbeth committed 2 years ago

f9d9e931

chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#19039)

hrmacbeth committed 2 years ago

fd5edc43

feat(topology/algebra/module/star): continuity results for star_modules (#19037)

eric-wieser committed 2 years ago

aa666983

chore(measure_theory/special_functions/basic): split (#19040)

hrmacbeth committed 2 years ago

83a66c87

chore(category_theory/monoidal/types): split file (#19035)

kim-em committed 2 years ago

95a87616

chore(algebra/category/Module/monoidal): split file (#19034)

kim-em committed 2 years ago

74403a3b

chore(data/set/Union_lift) generalize Union_lift to Sort (#19033)

ChrisHughes24 committed 2 years ago

5a4ea845

refactor(analysis/convex/specific_functions): split (#19031)

hrmacbeth committed 2 years ago

8f9fea08

feat(field_theory/minpoly/basic): `minpoly` is unaffected by injective `alg_hom`s (#19030)

eric-wieser committed 2 years ago

df0098f0

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

leanprover-community-bot committed 2 years ago

50251fd6

chore(number_theory/modular_forms): don't define jacobi_theta on subtype (#19029)

loefflerd committed 2 years ago

c720ca16

feat(algebra/category/Module/change_of_rings): coextension of scalars (#15958)

jjaassoonn committed 2 years ago

56b71f0b

feat(nat/factorial): add double factorials (#18994)

jakelev committed 2 years ago

7daeaf30

feat(analysis/convex/specific_functions): elementary convexity proofs (#19026)

hrmacbeth committed 2 years ago

a8b2226c

feat(geometry/manifold/vector_bundle/hom): the hom bundle is smooth (#18828)

fpvandoorn committed 2 years ago

c89fe2d5

feat(geometry/manifold/cont_mdiff_mfderiv): prove that mfderiv is smooth (#18827)

fpvandoorn committed 2 years ago

17fe3632

feat(analysis/inner_product_space/pi_L2): norms of basis vectors (#19020)

eric-wieser committed 2 years ago

8ff51ea9

feat(probability/kernel/cond_cdf): conditional cumulative distribution function (#18988)

RemyDegenne committed 2 years ago

20d57630

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

leanprover-community-bot committed 2 years ago

2ed2c631

feat(measure_theory/measure/hausdorff): `(μH[1] : measure ℝ) = volume` (#18982)

eric-wieser committed 2 years ago

b1859b6d

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)

leanprover-community-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

Older