AlternatingField.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Clearing the actual alternating fraction

The field formula for an integral alternating product is first converted to an identity in its coefficient ring. Arbitrary complex homomorphisms are then applied to that identity, without extending them to the field of fractions. The only nonvanishing inputs are the individual character values.

theorem OAI.CirculantHadamard.oddSubsetProduct_ne_zero line 21

theorem OAI.CirculantHadamard.cleared_alternatingProduct_identity line 31

Source documentation

An equality in the fraction field genuinely clears to the coefficient ring. The field embedding is used only to reflect this polynomial identity.

theorem cleared_alternatingProduct_identity {I : Type uI} {R : Type uR} {K : Type uK}
    [CommRing R] [Field K] (f : R →+* K) (hf : Function.Injective f)
    (t : Finset I) (x : Finset I → R) (z : R)
    (hx : ∀ S ⊆ t, f (x S) ≠ 0)
    (hz : f z = alternatingProduct t (fun S => f (x S))) :
    z * oddSubsetProduct t x = evenSubsetProduct t x := by
…

Mentions: OAI.CirculantHadamard.alternatingProduct, OAI.CirculantHadamard.oddSubsetProduct, OAI.CirculantHadamard.evenSubsetProduct

theorem OAI.CirculantHadamard.norm_hom_integral_alternatingProduct line 50

Source documentation

Once the actual alternating fraction belongs to the coefficient ring, every complex homomorphism has modulus one if each character value has the same positive modulus. Subset parity supplies the equal factor counts.

theorem norm_hom_integral_alternatingProduct {I : Type uI} {R : Type uR} {K : Type uK}
    [CommRing R] [Field K] (f : R →+* K) (hf : Function.Injective f)
    (t : Finset I) (ht : t.Nonempty) (x : Finset I → R) (z : R)
    (hx : ∀ S ⊆ t, f (x S) ≠ 0)
    (hz : f z = alternatingProduct t (fun S => f (x S)))
    (σ : R →+* ℂ) (c : ℝ) (hc : 0 < c)
    (hnorm : ∀ S ⊆ t, ‖σ (x S)‖ = c) : ‖σ z‖ = 1 := by
…

Mentions: OAI.CirculantHadamard.alternatingProduct