theorem proved term proof

`chi8_ne_zero_iff_odd`

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

formal statement (Lean)

 113theorem chi8_ne_zero_iff_odd (n : ℕ) : chi8 n ≠ 0 ↔ Odd n := by

proof body

Term-mode proof.

 114  -- `chi8 n = 0 ↔ Even n`, so negate and rewrite `¬Even ↔ Odd`.
 115  simpa [Nat.not_even_iff_odd] using (not_congr (chi8_eq_zero_iff_even n))
 116
 117/-- If `n` is coprime to `840`, then none of `2,3,5,7` divide `n`. -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
chi8 in IndisputableMonolith.NumberTheory.Primes.Modular decl_use
chi8_eq_zero_iff_even in IndisputableMonolith.NumberTheory.Primes.Modular decl_use
chi8 in IndisputableMonolith.NumberTheory.RecognitionTheta decl_use