Algebraic Combinatorics Blueprint

Blueprint Summary🔗

Overview
Total entries245completed: 245; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed245Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (245)
Definitions36completed: 36; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas163completed: 163; deps incomplete: 0; sorries: 0; no proof: 0
Theorems40completed: 40; deps incomplete: 0; sorries: 0; no proof: 0
Corollaries6completed: 6; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (36)
Theorem / Lemma / Corollary Index (209)
By parent groups (46)
Dyck words, Catalan numbers, and their generating function. (4)
The Exp and Log maps between series with constant term 0 and 1 . (2)
Finite sums and products in commutative rings. (4)
The standard algebraic rules for differentiating formal power series. (15)
The opening binomial-coefficient definitions and identities. (15)
Helper lemmas for the odd-factor product appearing in the central binomial coefficient formula. (2)
Polynomial evaluation as substitution into an algebra. (4)
Auxiliary power-series identities used by the examples. (5)
Newton's binomial formula and its negative-exponent variants. (5)
Division by the indeterminate x. (2)
Standard rules in commutative rings. (10)
Additive inverses in modules. (5)
The logarithm map on series with constant term one. (4)
Auxiliary lemmas used to put group structures on the Exp and Log domains. (3)
Invertibility criteria for formal power series. (2)
The ring and module structure on formal power series. (2)
The Fibonacci example and its generating-function formulas. (2)
The definition of the derivative and its first basic examples. (10)
Helper series and derivative identities. (4)
Power series with constant term one, and the first logarithmic constructions on them. (2)
Defining non-integer powers using Exp and Log . (3)
Auxiliary uniqueness and substitution lemmas for the inverse theorem. (5)
Helpers for division by x. (2)
How Exp turns addition into multiplication, and Log does the reverse. (3)
Basic exponent rules for the formal power-series power. (2)
The first infinite-family consequence: Log sends multipliable families to summable ones. (4)
The indeterminate x and its powers. (3)
The Newton binomial formula for arbitrary exponents. (3)
Converting between polynomial FPSs and actual polynomials. (2)
Why the substitution series is well-defined. (3)
Special values of polynomial evaluation. (3)
Solving a linear recurrence. (1)
Helper lemmas from the formalization. (9)
Auxiliary coefficient lemmas about multiples of powers of the indeterminate. (6)
Kronecker delta notation used in the substitution rules. (13)
The logarithmic derivative and its first basic identities. (6)
Further consequences of the exponent definition. (4)
Example: substitution applied to the Fibonacci generating function. (1)
Closure of polynomial FPSs under the ring and module operations. (10)
The exponential map on series with constant term zero. (3)
Polynomial power series and the polynomial ring inside formal power series. (3)
Coefficient formulas for inverses of formal power series. (5)
Helper lemmas for the explicit Catalan generating function. (4)
Essentially finite sums and summable families of formal power series. (2)
Generating functions of sequences. (1)
Defining composition of formal power series. (1)
Dependency insights
Tracked parent groups48Grouped health rollups for parents with more than one child entry.
Group health (48)
  • The opening binomial-coefficient definitions and identities.binomial_coefficients
    Grouped view over entries sharing the same parent.
    total: 16closed: 16local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • The standard algebraic rules for differentiating formal power series.derivative_rules
    Grouped view over entries sharing the same parent.
    total: 15closed: 15local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Kronecker delta notation used in the substitution rules.substitution_kronecker_delta
    Grouped view over entries sharing the same parent.
    total: 14closed: 14local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • The definition of the derivative and its first basic examples.derivatives_definition
    Grouped view over entries sharing the same parent.
    total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Closure of polynomial FPSs under the ring and module operations.polynomials_subring
    Grouped view over entries sharing the same parent.
    total: 10closed: 10local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Helper lemmas from the formalization.fps_helper_lemmas
    Grouped view over entries sharing the same parent.
    total: 10closed: 10local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Standard rules in commutative rings.commutative_rings_standard_rules
    Grouped view over entries sharing the same parent.
    total: 10closed: 10local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • The logarithmic derivative and its first basic identities.exp_log_loder
    Grouped view over entries sharing the same parent.
    total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Auxiliary coefficient lemmas about multiples of powers of the indeterminate.fps_misc_lemmas
    Grouped view over entries sharing the same parent.
    total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Dyck words, Catalan numbers, and their generating function.catalan_example
    Grouped view over entries sharing the same parent.
    total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Show all 38 more groups
    • The logarithm map on series with constant term one.non_integer_powers_log_map
      Grouped view over entries sharing the same parent.
      total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Additive inverses in modules.module_additive_inverses
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Auxiliary power-series identities used by the examples.auxiliary_generating_function_results
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Auxiliary uniqueness and substitution lemmas for the inverse theorem.exp_log_inverse_helpers
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Coefficient formulas for inverses of formal power series.fps_inverse_coefficients
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Newton's binomial formula and its negative-exponent variants.fps_newton_binomial
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Polynomial evaluation as substitution into an algebra.polynomials_evaluation
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The Fibonacci example and its generating-function formulas.fibonacci_sequence
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Defining non-integer powers using Exp and Log .non_integer_powers_power_definition
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Essentially finite sums and summable families of formal power series.fps_summable_families
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Finite sums and products in commutative rings.commutative_rings_finite_sums_products
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Further consequences of the exponent definition.non_integer_powers_further_rules
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Helper lemmas for the explicit Catalan generating function.catalan_gf_helpers
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Helper series and derivative identities.exp_log_derivative_helpers
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Polynomial power series and the polynomial ring inside formal power series.polynomials_definition
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The exponential map on series with constant term zero.non_integer_powers_exp_map
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The first infinite-family consequence: Log sends multipliable families to summable ones.exp_log_infinite_products
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The indeterminate x and its powers.fps_x_powers
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Auxiliary lemmas used to put group structures on the Exp and Log domains.exp_log_group_helpers
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Converting between polynomial FPSs and actual polynomials.polynomials_conversion
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Division by the indeterminate x.fps_div_by_x
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • How Exp turns addition into multiplication, and Log does the reverse.exp_log_group_structure
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Power series with constant term one, and the first logarithmic constructions on them.non_integer_powers_definition
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Special values of polynomial evaluation.polynomials_special_evaluation
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The Exp and Log maps between series with constant term 0 and 1 .exp_log_maps
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The Newton binomial formula for arbitrary exponents.non_integer_powers_newton
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The definition of formal power series, their basic operations, and coefficient notation.fps_definition_basic
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Why the substitution series is well-defined.substitution_well_definedness
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Basic exponent rules for the formal power-series power.non_integer_powers_rules
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Defining composition of formal power series.substitution_definition
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Example: substitution applied to the Fibonacci generating function.substitution_fibonacci_example
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Generating functions of sequences.fps_generating_functions
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Helper lemmas for the odd-factor product appearing in the central binomial coefficient formula.binom_helpers_two_n_choose_n
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Helpers for division by x.fps_div_by_x_helpers
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Invertibility criteria for formal power series.fps_invertibility
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Ring and algebra reminders used before polynomial evaluation.polynomials_ring_reminders
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • Solving a linear recurrence.recurrence_example
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • The ring and module structure on formal power series.fps_ring_structure
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner245
Missing effort245
Untagged245
Missing owner (245)
Missing effort (245)
Untagged (245)
Structure and coverage
Fully closed245Local code and ancestor closure are both complete.
No prerequisites (245)
No dependents (245)