PG002A

prime_field_polynomial_right_divides_empty

Every canonical divisor divides every encoding of the empty polynomial, using an actual empty quotient and actual empty product. No prime, nonzero modulus or nonempty divisor assumption is needed.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ db. ∀ dc. ∀ D. ∀ ab. ∀ ac. BetaPrefixInto(db,dc,D,p) → FpPolynomialRightDivides(p,db,dc,D,ab,ac,0)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixInto(b,c,l,B) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1

Actual proof prerequisites

prime_field_polynomial_right_divides_from_productmatrix_rank_bounded_prefix_empty · checked external prerequisiteprime_field_polynomial_convolution_empty · checked external prerequisiteprime_field_polynomial_power_coefficient_functional · checked external prerequisite
Original expanded first-order statement 
forall p db dc D ab ac. (forall fom_index_pfp_right_empty_divisor. (exists fom_gap_pfp_right_empty_divisor_index_bound. fom_gap_pfp_right_empty_divisor_index_bound + S (fom_index_pfp_right_empty_divisor) = D) -> exists fom_value_pfp_right_empty_divisor. ((((exists fom_beta_height_pfp_right_empty_divisor_entry. fom_beta_height_pfp_right_empty_divisor_entry + S (fom_value_pfp_right_empty_divisor) = S ((S (fom_index_pfp_right_empty_divisor)) * dc)) /\ exists fom_beta_quotient_pfp_right_empty_divisor_entry. db = fom_beta_quotient_pfp_right_empty_divisor_entry * S ((S (fom_index_pfp_right_empty_divisor)) * dc) + (fom_value_pfp_right_empty_divisor))) /\ (exists fom_gap_pfp_right_empty_divisor_value_bound. fom_gap_pfp_right_empty_divisor_value_bound + S (fom_value_pfp_right_empty_divisor) = p))) -> (((forall fom_index_pfp_right_empty_result_canonical. (exists fom_gap_pfp_right_empty_result_canonical_index_bound. fom_gap_pfp_right_empty_result_canonical_index_bound + S (fom_index_pfp_right_empty_result_canonical) = 0) -> exists fom_value_pfp_right_empty_result_canonical. ((((exists fom_beta_height_pfp_right_empty_result_canonical_entry. fom_beta_height_pfp_right_empty_result_canonical_entry + S (fom_value_pfp_right_empty_result_canonical) = S ((S (fom_index_pfp_right_empty_result_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_empty_result_canonical_entry. ab = fom_beta_quotient_pfp_right_empty_result_canonical_entry * S ((S (fom_index_pfp_right_empty_result_canonical)) * ac) + (fom_value_pfp_right_empty_result_canonical))) /\ (exists fom_gap_pfp_right_empty_result_canonical_value_bound. fom_gap_pfp_right_empty_result_canonical_value_bound + S (fom_value_pfp_right_empty_result_canonical) = p))) /\ ((exists pfrd_qb_right_empty_result pfrd_qc_right_empty_result pfrd_qlen_right_empty_result pfrd_pb_right_empty_result pfrd_pc_right_empty_result pfrd_plen_right_empty_result. ((((forall fom_index_pfp_right_empty_result_productleft. (exists fom_gap_pfp_right_empty_result_productleft_index_bound. fom_gap_pfp_right_empty_result_productleft_index_bound + S (fom_index_pfp_right_empty_result_productleft) = pfrd_qlen_right_empty_result) -> exists fom_value_pfp_right_empty_result_productleft. ((((exists fom_beta_height_pfp_right_empty_result_productleft_entry. fom_beta_height_pfp_right_empty_result_productleft_entry + S (fom_value_pfp_right_empty_result_productleft) = S ((S (fom_index_pfp_right_empty_result_productleft)) * pfrd_qc_right_empty_result)) /\ exists fom_beta_quotient_pfp_right_empty_result_productleft_entry. pfrd_qb_right_empty_result = fom_beta_quotient_pfp_right_empty_result_productleft_entry * S ((S (fom_index_pfp_right_empty_result_productleft)) * pfrd_qc_right_empty_result) + (fom_value_pfp_right_empty_result_productleft))) /\ (exists fom_gap_pfp_right_empty_result_productleft_value_bound. fom_gap_pfp_right_empty_result_productleft_value_bound + S (fom_value_pfp_right_empty_result_productleft) = p))) /\ (((forall fom_index_pfp_right_empty_result_productright. (exists fom_gap_pfp_right_empty_result_productright_index_bound. fom_gap_pfp_right_empty_result_productright_index_bound + S (fom_index_pfp_right_empty_result_productright) = D) -> exists fom_value_pfp_right_empty_result_productright. ((((exists fom_beta_height_pfp_right_empty_result_productright_entry. fom_beta_height_pfp_right_empty_result_productright_entry + S (fom_value_pfp_right_empty_result_productright) = S ((S (fom_index_pfp_right_empty_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_empty_result_productright_entry. db = fom_beta_quotient_pfp_right_empty_result_productright_entry * S ((S (fom_index_pfp_right_empty_result_productright)) * dc) + (fom_value_pfp_right_empty_result_productright))) /\ (exists fom_gap_pfp_right_empty_result_productright_value_bound. fom_gap_pfp_right_empty_result_productright_value_bound + S (fom_value_pfp_right_empty_result_productright) = p))) /\ (((((((pfrd_qlen_right_empty_result)=0 \/ (D)=0) /\ (((pfrd_plen_right_empty_result)=0)))) \/ (((~((pfrd_qlen_right_empty_result)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_empty_result)+(D)=S (pfrd_plen_right_empty_result)))))))) /\ ((forall pfc_index_right_empty_result_productcoefficients. (exists pfa_gap_right_empty_result_productcoefficientsbound. pfa_gap_right_empty_result_productcoefficientsbound + S (pfc_index_right_empty_result_productcoefficients) = (pfrd_plen_right_empty_result)) -> exists pfc_value_right_empty_result_productcoefficients. ((((exists ff_h_pfp_right_empty_result_productcoefficientsentry. ff_h_pfp_right_empty_result_productcoefficientsentry + S (pfc_value_right_empty_result_productcoefficients) = S ((S (pfc_index_right_empty_result_productcoefficients)) * pfrd_pc_right_empty_result)) /\ exists ff_q_pfp_right_empty_result_productcoefficientsentry. pfrd_pb_right_empty_result = ff_q_pfp_right_empty_result_productcoefficientsentry * S ((S (pfc_index_right_empty_result_productcoefficients)) * pfrd_pc_right_empty_result) + (pfc_value_right_empty_result_productcoefficients))) /\ ((exists pfc_terms_code_right_empty_result_productcoefficientscoefficient pfc_terms_scale_right_empty_result_productcoefficientscoefficient pfc_natural_sum_right_empty_result_productcoefficientscoefficient. ((forall pfc_index_right_empty_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_empty_result_productcoefficientscoefficientdiagonalbound. pfa_gap_right_empty_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_empty_result_productcoefficients))) -> exists pfc_value_right_empty_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_empty_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_empty_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_empty_result_productcoefficientscoefficient = ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_empty_result_productcoefficientscoefficient) + (pfc_value_right_empty_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm pfc_left_right_empty_result_productcoefficientscoefficientdiagonalterm pfc_right_right_empty_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)+pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm=(pfc_index_right_empty_result_productcoefficients)) /\ ((((((exists pfa_gap_right_empty_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_empty_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_empty_result)) /\ ((((exists ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_empty_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_empty_result)) /\ exists ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_empty_result = ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_empty_result) + (pfc_left_right_empty_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_empty_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_empty_result_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_empty_result)=(pfc_index_right_empty_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_empty_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_empty_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_empty_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_empty_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_empty_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_empty_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_empty_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_empty_result_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_empty_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_empty_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_empty_result_productcoefficientscoefficientdiagonal)=pfc_left_right_empty_result_productcoefficientscoefficientdiagonalterm*pfc_right_right_empty_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_empty_result_productcoefficientscoefficientsum fs_v_pfc_right_empty_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_empty_result_productcoefficientscoefficientsum = fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_empty_result_productcoefficientscoefficient) = S ((S (S (pfc_index_right_empty_result_productcoefficients))) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_empty_result_productcoefficientscoefficientsum = fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_empty_result_productcoefficients))) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum) + (pfc_natural_sum_right_empty_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_empty_result_productcoefficients)) -> exists fs_a_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_empty_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_empty_result_productcoefficientscoefficient = fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_empty_result_productcoefficientscoefficient) + (fs_a_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_empty_result_productcoefficientscoefficientsum = fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum) + (fs_r_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_empty_result_productcoefficientscoefficientsum = fs_q_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_empty_result_productcoefficientscoefficientsum) + (fs_s_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_empty_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_empty_result_productcoefficientscoefficientresiduebound. pfa_gap_right_empty_result_productcoefficientscoefficientresiduebound + S (pfc_value_right_empty_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_empty_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_empty_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_empty_result_productcoefficientscoefficient) + (p) * pfa_offset_left_right_empty_result_productcoefficientscoefficientresiduecongruence = (pfc_value_right_empty_result_productcoefficients) + (p) * pfa_offset_right_right_empty_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_empty_result_target pfrep_left_right_empty_result_target pfrep_right_right_empty_result_target. ((exists pfrep_position_right_empty_result_targetfirst. ((pfrep_position_right_empty_result_targetfirst+S (pfrep_power_right_empty_result_target)=(pfrd_plen_right_empty_result)) /\ ((((exists ff_h_pfp_right_empty_result_targetfirstentry. ff_h_pfp_right_empty_result_targetfirstentry + S (pfrep_left_right_empty_result_target) = S ((S (pfrep_position_right_empty_result_targetfirst)) * pfrd_pc_right_empty_result)) /\ exists ff_q_pfp_right_empty_result_targetfirstentry. pfrd_pb_right_empty_result = ff_q_pfp_right_empty_result_targetfirstentry * S ((S (pfrep_position_right_empty_result_targetfirst)) * pfrd_pc_right_empty_result) + (pfrep_left_right_empty_result_target)))))) \/ (((exists pfrep_gap_right_empty_result_targetfirstoutside. pfrep_gap_right_empty_result_targetfirstoutside+(pfrd_plen_right_empty_result)=(pfrep_power_right_empty_result_target)) /\ (((pfrep_left_right_empty_result_target)=0))))) -> ((exists pfrep_position_right_empty_result_targetsecond. ((pfrep_position_right_empty_result_targetsecond+S (pfrep_power_right_empty_result_target)=(0)) /\ ((((exists ff_h_pfp_right_empty_result_targetsecondentry. ff_h_pfp_right_empty_result_targetsecondentry + S (pfrep_right_right_empty_result_target) = S ((S (pfrep_position_right_empty_result_targetsecond)) * ac)) /\ exists ff_q_pfp_right_empty_result_targetsecondentry. ab = ff_q_pfp_right_empty_result_targetsecondentry * S ((S (pfrep_position_right_empty_result_targetsecond)) * ac) + (pfrep_right_right_empty_result_target)))))) \/ (((exists pfrep_gap_right_empty_result_targetsecondoutside. pfrep_gap_right_empty_result_targetsecondoutside+(0)=(pfrep_power_right_empty_result_target)) /\ (((pfrep_right_right_empty_result_target)=0))))) -> pfrep_left_right_empty_result_target=pfrep_right_right_empty_result_target)))))))

Complete tactic proof in conservative notation

All 56 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

56 script commands · 9 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
prime field polynomial right divides from product
01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro db
  3. L3
    intro dc
  4. L4
    intro D
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro hD
02Use earlier factsL8–17

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L8
    specialize prime_field_polynomial_right_divides_from_product (p)
  2. L9
    specialize prime_field_polynomial_right_divides_from_product (db)
  3. L10
    specialize prime_field_polynomial_right_divides_from_product (dc)
  4. L11
    specialize prime_field_polynomial_right_divides_from_product (D)
  5. L12
    specialize prime_field_polynomial_right_divides_from_product (ab)
  6. L13
    specialize prime_field_polynomial_right_divides_from_product (ac)
  7. L14
    specialize prime_field_polynomial_right_divides_from_product (0)
  8. L15
    specialize prime_field_polynomial_right_divides_from_product (0)
  9. L16
    specialize prime_field_polynomial_right_divides_from_product (0)
  10. L17
    specialize prime_field_polynomial_right_divides_from_product (0)
03Use earlier factsL18–27

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L18
    specialize prime_field_polynomial_right_divides_from_product (ab)
  2. L19
    specialize prime_field_polynomial_right_divides_from_product (ac)
  3. L20
    specialize prime_field_polynomial_right_divides_from_product (0)
  4. L21
    apply prime_field_polynomial_right_divides_from_product
  5. L22
    specialize matrix_rank_bounded_prefix_empty (ab)
  6. L23
    specialize matrix_rank_bounded_prefix_empty (ac)
  7. L24
    specialize matrix_rank_bounded_prefix_empty (p)
  8. L25
    apply matrix_rank_bounded_prefix_empty
  9. L26
    specialize prime_field_polynomial_convolution_empty (p)
  10. L27
    specialize prime_field_polynomial_convolution_empty (0)
04Use earlier factsL28–37

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L28
    specialize prime_field_polynomial_convolution_empty (0)
  2. L29
    specialize prime_field_polynomial_convolution_empty (0)
  3. L30
    specialize prime_field_polynomial_convolution_empty (db)
  4. L31
    specialize prime_field_polynomial_convolution_empty (dc)
  5. L32
    specialize prime_field_polynomial_convolution_empty (D)
  6. L33
    specialize prime_field_polynomial_convolution_empty (ab)
  7. L34
    specialize prime_field_polynomial_convolution_empty (ac)
  8. L35
    apply prime_field_polynomial_convolution_empty
  9. L36
    specialize matrix_rank_bounded_prefix_empty (0)
  10. L37
    specialize matrix_rank_bounded_prefix_empty (0)
05Use earlier factsL38–40

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    specialize matrix_rank_bounded_prefix_empty (p)
  2. L39
    apply matrix_rank_bounded_prefix_empty
  3. L40
    exact hD
06Separate the logical casesL41–41

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L41
    left
07Calculate and transport equalitiesL42–42

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    refl
08Fix variables and assumptionsL43–47

Work with arbitrary variables or the premises of the current implication.

  1. L43
    intro k
  2. L44
    intro a
  3. L45
    intro r
  4. L46
    intro ha
  5. L47
    intro hr
09Use earlier factsL48–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    specialize prime_field_polynomial_power_coefficient_functional (ab)
  2. L49
    specialize prime_field_polynomial_power_coefficient_functional (ac)
  3. L50
    specialize prime_field_polynomial_power_coefficient_functional (0)
  4. L51
    specialize prime_field_polynomial_power_coefficient_functional (k)
  5. L52
    specialize prime_field_polynomial_power_coefficient_functional (a)
  6. L53
    specialize prime_field_polynomial_power_coefficient_functional (r)
  7. L54
    apply prime_field_polynomial_power_coefficient_functional
  8. L55
    exact ha
  9. L56
    exact hr

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro D
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro hD
  8. 0008specialize prime_field_polynomial_right_divides_from_product (p)
  9. 0009specialize prime_field_polynomial_right_divides_from_product (db)
  10. 0010specialize prime_field_polynomial_right_divides_from_product (dc)
  11. 0011specialize prime_field_polynomial_right_divides_from_product (D)
  12. 0012specialize prime_field_polynomial_right_divides_from_product (ab)
  13. 0013specialize prime_field_polynomial_right_divides_from_product (ac)
  14. 0014specialize prime_field_polynomial_right_divides_from_product (0)
  15. 0015specialize prime_field_polynomial_right_divides_from_product (0)
  16. 0016specialize prime_field_polynomial_right_divides_from_product (0)
  17. 0017specialize prime_field_polynomial_right_divides_from_product (0)
  18. 0018specialize prime_field_polynomial_right_divides_from_product (ab)
  19. 0019specialize prime_field_polynomial_right_divides_from_product (ac)
  20. 0020specialize prime_field_polynomial_right_divides_from_product (0)
  21. 0021apply prime_field_polynomial_right_divides_from_product
  22. 0022specialize matrix_rank_bounded_prefix_empty (ab)
  23. 0023specialize matrix_rank_bounded_prefix_empty (ac)
  24. 0024specialize matrix_rank_bounded_prefix_empty (p)
  25. 0025apply matrix_rank_bounded_prefix_empty
  26. 0026specialize prime_field_polynomial_convolution_empty (p)
  27. 0027specialize prime_field_polynomial_convolution_empty (0)
  28. 0028specialize prime_field_polynomial_convolution_empty (0)
  29. 0029specialize prime_field_polynomial_convolution_empty (0)
  30. 0030specialize prime_field_polynomial_convolution_empty (db)
  31. 0031specialize prime_field_polynomial_convolution_empty (dc)
  32. 0032specialize prime_field_polynomial_convolution_empty (D)
  33. 0033specialize prime_field_polynomial_convolution_empty (ab)
  34. 0034specialize prime_field_polynomial_convolution_empty (ac)
  35. 0035apply prime_field_polynomial_convolution_empty
  36. 0036specialize matrix_rank_bounded_prefix_empty (0)
  37. 0037specialize matrix_rank_bounded_prefix_empty (0)
  38. 0038specialize matrix_rank_bounded_prefix_empty (p)
  39. 0039apply matrix_rank_bounded_prefix_empty
  40. 0040exact hD
  41. 0041left
  42. 0042refl
  43. 0043intro k
  44. 0044intro a
  45. 0045intro r
  46. 0046intro ha
  47. 0047intro hr
  48. 0048specialize prime_field_polynomial_power_coefficient_functional (ab)
  49. 0049specialize prime_field_polynomial_power_coefficient_functional (ac)
  50. 0050specialize prime_field_polynomial_power_coefficient_functional (0)
  51. 0051specialize prime_field_polynomial_power_coefficient_functional (k)
  52. 0052specialize prime_field_polynomial_power_coefficient_functional (a)
  53. 0053specialize prime_field_polynomial_power_coefficient_functional (r)
  54. 0054apply prime_field_polynomial_power_coefficient_functional
  55. 0055exact ha
  56. 0056exact hr