theorem proved term proof

`finitePrimeLedgerPartition_insert_nonprime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  37theorem finitePrimeLedgerPartition_insert_nonprime
  38    (s : ℂ) (S : Finset ℕ) {n : ℕ} (hnS : n ∉ S) (hn : ¬ Nat.Prime n) :
  39    finitePrimeLedgerPartition s (insert n S) = finitePrimeLedgerPartition s S := by

proof body

Term-mode proof.

  40  unfold finitePrimeLedgerPartition
  41  simp [hnS, hn]
  42
  43/-- Inserting a new prime multiplies the partition by its local factor. -/

depends on (3)

Lean names referenced from this declaration's body.

finitePrimeLedgerPartition in IndisputableMonolith.NumberTheory.EulerLedgerPartition decl_use
Prime in IndisputableMonolith.NumberTheory.Primes.Basic decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use