Pinned Loading

1. power-series-ring-is-noetherian- power-series-ring-is-noetherian- Public

   This file formalized that if $R$ is noetherian, then its power series ring $R[[X]]$ is also noetherian

   Lean 2

2. L1-convergence-of-Fejer-sum L1-convergence-of-Fejer-sum Public

   Formalize L1 convergence of Fejer sum for Lebesgue integrable functions on a circle using mathlib in lean4

   Lean 1

3. Some-category-theory-exercises Some-category-theory-exercises Public

   形式化一些网上找的范畴论的习题

   Lean

4. Some-analysis-exercises Some-analysis-exercises Public

   形式化一些网上找的分析的习题

   Lean

5. l1-ismorphic-to-c0-dual l1-ismorphic-to-c0-dual Public

   Formalize the construction of the ismorphism from l1 (the space of summable sequences over the real numbers) to the dual space of c0 (the space of sequences converging to 0 endowed with sup norm)

   Lean 1