1. OAI
  2. NumberTheory
  3. DirichletL
  4. GaussSum
  5. SexticNormalization
import OAI.NumberTheory.DirichletL.GaussSum.CubicNormalizationnamespace OAInoncomputable sectionopen scoped BigOperatorsopen MulChar AddCharopen scoped BigOperatorsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped FourierTransform SchwartzMapopen Finset Complexopen scoped Classicalopen scoped Classicalnamespace ActualEisensteinCubicsectionopen EisensteinEmbedding ConcreteTraceCRT PrimitiveTracenoncomputable def breveGamma1 (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) : ℂ := gaussSum (canonicalSextic P hgood) (hP.symm ▸ eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp) / (‖eisEmbedding p‖ : ℂ)noncomputable def breveGamma3 (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) : ℂ := gaussSum (canonicalSextic P hgood ^ 3) (hP.symm ▸ eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp) / (‖eisEmbedding p‖ : ℂ)theorem canonicalSextic_pow_three_quadratic (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) : canonicalSextic P hgood ^ 3 = (quadraticChar (O ⧸ P)).ringHomComp (Int.castRingHom ℂ) := P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ P⊢ canonicalSextic P hgood ^ 3 = (quadraticChar (O ⧸ P)).ringHomComp (Int.castRingHom ℂ) P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ P⊢ (sexticChar P hgood).ringHomComp eisEmbedding ^ 3 = (quadraticChar (O ⧸ P)).ringHomComp (Int.castRingHom ℂ) P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ P⊢ (OAI.ActualEisensteinCubic.quadraticCharO✝ P).ringHomComp eisEmbedding = (quadraticChar (O ⧸ P)).ringHomComp (Int.castRingHom ℂ) P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Px:(O ⧸ P)ˣ⊢ ((OAI.ActualEisensteinCubic.quadraticCharO✝ P).ringHomComp eisEmbedding) ↑x = ((quadraticChar (O ⧸ P)).ringHomComp (Int.castRingHom ℂ)) ↑x P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Px:(O ⧸ P)ˣ⊢ eisEmbedding ↑((quadraticChar (O ⧸ P)) ↑x) = ↑((quadraticChar (O ⧸ P)) ↑x) All goals completed! 🐙theorem breveGamma1_gamma2_relation (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (hchar : ringChar (O ⧸ P) ≠ 2) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) (hprimary : lambda ^ 2 ∣ p - 1) : breveGamma1 P hgood p hP hp * breveGamma2 P hgood p hP hp = (canonicalSextic P hgood (Ideal.Quotient.mk P (4 : O)))⁻¹ * breveGamma3 P hgood p hP hp * (breveGamma2 P hgood p hP hp) ^ 3 := P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2p:OhP:P = Ideal.span {p}hp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1⊢ breveGamma1 P hgood p hP hp * breveGamma2 P hgood p hP hp = ((canonicalSextic P hgood) ((Ideal.Quotient.mk P) 4))⁻¹ * breveGamma3 P hgood p hP hp * breveGamma2 P hgood p hP hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgood⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitive⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hmul:χ 4 * (gaussSum χ ψ / s) * (gaussSum (χ ^ 2) ψ / s) = gaussSum (χ ^ 3) ψ / s * (gaussSum (χ ^ 2) ψ / s) ^ 3⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hmul:χ 4 * (gaussSum χ ψ / s) * (gaussSum (χ ^ 2) ψ / s) = gaussSum (χ ^ 3) ψ / s * (gaussSum (χ ^ 2) ψ / s) ^ 3hfour:4 ≠ 0⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hmul:χ 4 * (gaussSum χ ψ / s) * (gaussSum (χ ^ 2) ψ / s) = gaussSum (χ ^ 3) ψ / s * (gaussSum (χ ^ 2) ψ / s) ^ 3hfour:4 ≠ 0hχfour:χ 4 ≠ 0⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hfour:4 ≠ 0hχfour:χ 4 ≠ 0hmul:χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = ((canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) 4))⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hfour:4 ≠ 0hχfour:χ 4 ≠ 0hmul:χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = (χ 4)⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 calc breveGamma1 (Ideal.span {p}) hgood p rfl hp * breveGamma2 (Ideal.span {p}) hgood p rfl hp = (χ 4)⁻¹ * (χ 4 * breveGamma1 (Ideal.span {p}) hgood p rfl hp * breveGamma2 (Ideal.span {p}) hgood p rfl hp) := p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hfour:4 ≠ 0hχfour:χ 4 ≠ 0hmul:χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = (χ 4)⁻¹ * (χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp) All goals completed! 🐙 _ = (χ 4)⁻¹ * (breveGamma3 (Ideal.span {p}) hgood p rfl hp * breveGamma2 (Ideal.span {p}) hgood p rfl hp ^ 3) := p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hfour:4 ≠ 0hχfour:χ 4 ≠ 0hmul:χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3⊢ (χ 4)⁻¹ * (χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp) = (χ 4)⁻¹ * (breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3) All goals completed! 🐙 _ = _ := p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ2:χ ^ 2 ≠ 1hχ4:χ ^ 4 ≠ 1hχ3:χ ^ 3 = (quadraticChar (O ⧸ Ideal.span {p})).ringHomComp (Int.castRingHom ℂ)hχ6:χ ^ 6 = 1hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0hfour:4 ≠ 0hχfour:χ 4 ≠ 0hmul:χ 4 * breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp = breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3⊢ (χ 4)⁻¹ * (breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3) = (χ 4)⁻¹ * breveGamma3 (Ideal.span {p}) hgood p ⋯ hp * breveGamma2 (Ideal.span {p}) hgood p ⋯ hp ^ 3 All goals completed! 🐙endsectionopen EisensteinEmbedding ConcreteTraceCRT IdealGaussCRTprivate theorem breveE_period_O (x : O) : ShortDraftTrace.breveE (eisEmbedding x) = 1 := x:O⊢ ShortDraftTrace.breveE (eisEmbedding x) = 1 x:Oa:ℤb:ℤhx:x = ↑a + ↑b * pb.gen⊢ ShortDraftTrace.breveE (eisEmbedding x) = 1 x:Oa:ℤb:ℤhx:x = ↑a + ↑b * pb.gen⊢ ShortDraftTrace.breveE (eisEmbedding (↑a + ↑b * pb.gen)) = 1 x:Oa:ℤb:ℤhx:x = ↑a + ↑b * pb.gen⊢ ShortDraftTrace.breveE ((embedding omega3 omega3_sq) (↑a + ↑b * pb.gen)) = 1 x:Oa:ℤb:ℤhx:x = ↑a + ↑b * pb.gen⊢ ShortDraftTrace.breveE (↑a + ↑b * omega3) = 1 x:Oa:ℤb:ℤhx:x = ↑a + ↑b * pb.gen⊢ ShortDraftTrace.breveE (↑a + ↑b * ShortDraftTrace.ω₃) = 1 All goals completed! 🐙private noncomputable def eisBreveModChar (p : O) (hp : p ≠ 0) : AddChar (O ⧸ Ideal.span {p}) ℂ := traceModChar eisEmbedding ShortDraftTrace.breveE 1 p (eisEmbedding_ne_zero hp) one_ne_zero (p:Ohp:p ≠ 0⊢ ∀ (x : EisensteinEmbedding.O), ShortDraftTrace.breveE (eisEmbedding x / 1) = 1 p:Ohp:p ≠ 0x:EisensteinEmbedding.O⊢ ShortDraftTrace.breveE (eisEmbedding x / 1) = 1 All goals completed! 🐙)theorem eisEmbedding_traceLambda : eisEmbedding traceLambda = eisLam := ⊢ eisEmbedding traceLambda = eisLam hgen:pb.gen = omega⊢ eisEmbedding traceLambda = eisLam hgen:pb.gen = omega⊢ (embedding omega3 omega3_sq) (1 + 2 * omega) = 1 + 2 * omega3 hgen:pb.gen = omega⊢ (embedding omega3 omega3_sq) (1 + 2 * pb.gen) = 1 + 2 * omega3 All goals completed! 🐙private theorem eisBreveModChar_eq_mulShift (p : O) (hp : p ≠ 0) : eisBreveModChar p hp = (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift (Ideal.Quotient.mk (Ideal.span {p}) traceLambda) := p:Ohp:p ≠ 0⊢ eisBreveModChar p hp = (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift ((Ideal.Quotient.mk (Ideal.span {p})) traceLambda) p:Ohp:p ≠ 0⊢ ∀ (x : O ⧸ Ideal.span {p}), (eisBreveModChar p hp) x = ((eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift ((Ideal.Quotient.mk (Ideal.span {p})) traceLambda)) x p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}⊢ (eisBreveModChar p hp) z = ((eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift ((Ideal.Quotient.mk (Ideal.span {p})) traceLambda)) z p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}⊢ ∀ (a : O), (eisBreveModChar p hp) (Quotient.mk'' a) = ((eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift ((Ideal.Quotient.mk (Ideal.span {p})) traceLambda)) (Quotient.mk'' a) p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}x:O⊢ (eisBreveModChar p hp) (Quotient.mk'' x) = ((eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp).mulShift ((Ideal.Quotient.mk (Ideal.span {p})) traceLambda)) (Quotient.mk'' x) p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}x:O⊢ ShortDraftTrace.breveE (eisEmbedding x / (eisEmbedding p * 1)) = ShortDraftTrace.breveE (eisEmbedding (traceLambda * x) / (eisEmbedding p * eisLam)) p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}x:O⊢ eisEmbedding x / (eisEmbedding p * 1) = eisEmbedding (traceLambda * x) / (eisEmbedding p * eisLam) p:Ohp:p ≠ 0z:O ⧸ Ideal.span {p}x:O⊢ eisEmbedding x / (eisEmbedding p * 1) = eisLam * eisEmbedding x / (eisEmbedding p * eisLam) All goals completed! 🐙endsectionopen EisensteinEmbedding ConcreteTraceCRT PrimitiveTracenoncomputable def breveLocalG (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) : ℂ := (canonicalSextic P hgood (Ideal.Quotient.mk P (4 : O)))⁻¹ * breveGamma3 P hgood p hP hptheorem breveGamma1_gamma2_eq_neg_alpha_G (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (hchar : ringChar (O ⧸ P) ≠ 2) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) (hprimary : lambda ^ 2 ∣ p - 1) : breveGamma1 P hgood p hP hp * breveGamma2 P hgood p hP hp = (-(eisEmbedding p) / (‖eisEmbedding p‖ : ℂ)) * breveLocalG P hgood p hP hp := P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2p:OhP:P = Ideal.span {p}hp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1⊢ breveGamma1 P hgood p hP hp * breveGamma2 P hgood p hP hp = -eisEmbedding p / ↑‖eisEmbedding p‖ * breveLocalG P hgood p hP hp P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2p:OhP:P = Ideal.span {p}hp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1⊢ ((canonicalSextic P hgood) ((Ideal.Quotient.mk P) 4))⁻¹ * breveGamma3 P hgood p hP hp * (-eisEmbedding p / ↑‖eisEmbedding p‖) = -eisEmbedding p / ↑‖eisEmbedding p‖ * breveLocalG P hgood p hP hp P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2p:OhP:P = Ideal.span {p}hp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1⊢ ((canonicalSextic P hgood) ((Ideal.Quotient.mk P) 4))⁻¹ * breveGamma3 P hgood p hP hp * (-eisEmbedding p / ↑‖eisEmbedding p‖) = -eisEmbedding p / ↑‖eisEmbedding p‖ * (((canonicalSextic P hgood) ((Ideal.Quotient.mk P) 4))⁻¹ * breveGamma3 P hgood p hP hp) All goals completed! 🐙endopen EisensteinEmbedding ConcreteTraceCRT ConcreteBreveEnoncomputable def breveGamma2Product (a b : O) (ha : a ≠ 0) (hb : b ≠ 0) [haMax : (Ideal.span {a}).IsMaximal] [hbMax : (Ideal.span {b}).IsMaximal] (hgooda : lambda ∉ Ideal.span {a}) (hgoodb : lambda ∉ Ideal.span {b}) : ℂ := a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}this:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}this✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}this✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgooda⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}this✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodb⊢ ℂ All goals completed! 🐙theorem breveGamma2Product_crt (a b : O) (ha : a ≠ 0) (hb : b ≠ 0) [haMax : (Ideal.span {a}).IsMaximal] [hbMax : (Ideal.span {b}).IsMaximal] (hgooda : lambda ∉ Ideal.span {a}) (hgoodb : lambda ∉ Ideal.span {b}) (hcop : IsCoprime (Ideal.span {a}) (Ideal.span {b})) : breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda (Ideal.Quotient.mk (Ideal.span {a}) b)) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb (Ideal.Quotient.mk (Ideal.span {b}) a)) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a rfl ha * breveGamma2 (Ideal.span {b}) hgoodb b rfl hb := a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝¹:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this:Finite (O ⧸ Ideal.span {a}) := ···⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝:Finite (O ⧸ Ideal.span {a}) := ···this:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝³:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝²:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝¹:Finite (O ⧸ Ideal.span {a}) := ···this✝:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this:Finite (O ⧸ Ideal.span {b}) := ···⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgooda⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodb⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ breveGamma2Product a b ha hb hgooda hgoodb = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ (∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x) / ↑‖eisEmbedding (a * b)‖ = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ χa ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * breveGamma2 (Ideal.span {a}) hgooda a ⋯ ha * breveGamma2 (Ideal.span {b}) hgoodb b ⋯ hb a:Ob:Oha:a ≠ 0hb:b ≠ 0haMax:(Ideal.span {a}).IsMaximalhbMax:(Ideal.span {b}).IsMaximalhgooda:lambda ∉ Ideal.span {a}hgoodb:lambda ∉ Ideal.span {b}hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})this✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂ := canonicalSextic (Ideal.span {a}) hgoodaχb:MulChar (O ⧸ Ideal.span {b}) ℂ := canonicalSextic (Ideal.span {b}) hgoodbhsum:∑ x, (χa ^ 2) ((Ideal.Quotient.factor ⋯) x) * (χb ^ 2) ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = (χa ^ 2) ((Ideal.Quotient.mk (Ideal.span {a})) b) * (χb ^ 2) ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ χa ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * gaussSum (χa ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum (χb ^ 2) (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = (canonicalSextic (Ideal.span {a}) hgooda) ((Ideal.Quotient.mk (Ideal.span {a})) b) ^ 2 * (canonicalSextic (Ideal.span {b}) hgoodb) ((Ideal.Quotient.mk (Ideal.span {b})) a) ^ 2 * (gaussSum (canonicalSextic (Ideal.span {a}) hgooda ^ 2) (⋯ ▸ eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) / ↑‖eisEmbedding a‖) * (gaussSum (canonicalSextic (Ideal.span {b}) hgoodb ^ 2) (⋯ ▸ eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / ↑‖eisEmbedding b‖) All goals completed! 🐙end ActualEisensteinCubicnamespace ConcreteBreveEopen EisensteinEmbedding ConcreteTraceCRTnoncomputable def normalizedTraceGauss (a : O) (ha : a ≠ 0) (χ : MulChar (O ⧸ Ideal.span {a}) ℂ) : ℂ := a:Oha:a ≠ 0χ:MulChar (O ⧸ Ideal.span {a}) ℂ⊢ ℂ a:Oha:a ≠ 0χ:MulChar (O ⧸ Ideal.span {a}) ℂthis:Finite (O ⧸ Ideal.span {a}) := ···⊢ ℂ a:Oha:a ≠ 0χ:MulChar (O ⧸ Ideal.span {a}) ℂthis✝:Finite (O ⧸ Ideal.span {a}) := ···this:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})⊢ ℂ All goals completed! 🐙noncomputable def normalizedTraceGaussProduct (a b : O) (ha : a ≠ 0) (hb : b ≠ 0) (χa : MulChar (O ⧸ Ideal.span {a}) ℂ) (χb : MulChar (O ⧸ Ideal.span {b}) ℂ) : ℂ := a:Ob:Oha:a ≠ 0hb:b ≠ 0χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂ⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···⊢ ℂ a:Ob:Oha:a ≠ 0hb:b ≠ 0χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})⊢ ℂ All goals completed! 🐙theorem normalizedTraceGaussProduct_crt (a b : O) (ha : a ≠ 0) (hb : b ≠ 0) (hcop : IsCoprime (Ideal.span {a}) (Ideal.span {b})) (χa : MulChar (O ⧸ Ideal.span {a}) ℂ) (χb : MulChar (O ⧸ Ideal.span {b}) ℂ) : normalizedTraceGaussProduct a b ha hb χa χb = χa (Ideal.Quotient.mk (Ideal.span {a}) b) * χb (Ideal.Quotient.mk (Ideal.span {b}) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb := a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂ⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝¹:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this:Finite (O ⧸ Ideal.span {a}) := ···⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝²:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝:Finite (O ⧸ Ideal.span {a}) := ···this:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝³:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝²:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝¹:Finite (O ⧸ Ideal.span {a}) := ···this✝:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this:Finite (O ⧸ Ideal.span {b}) := ···⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})hsum:∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})hsum:∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ normalizedTraceGaussProduct a b ha hb χa χb = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})hsum:∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ (∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x) / ↑‖eisEmbedding (a * b)‖ = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})hsum:∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * normalizedTraceGauss a ha χa * normalizedTraceGauss b hb χb a:Ob:Oha:a ≠ 0hb:b ≠ 0hcop:IsCoprime (Ideal.span {a}) (Ideal.span {b})χa:MulChar (O ⧸ Ideal.span {a}) ℂχb:MulChar (O ⧸ Ideal.span {b}) ℂthis✝⁴:Finite (O ⧸ Ideal.span {a} * Ideal.span {b}) := ···this✝³:Fintype (O ⧸ Ideal.span {a} * Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {a} * Ideal.span {b})this✝²:Finite (O ⧸ Ideal.span {a}) := ···this✝¹:Fintype (O ⧸ Ideal.span {a}) := Fintype.ofFinite (O ⧸ Ideal.span {a})this✝:Finite (O ⧸ Ideal.span {b}) := ···this:Fintype (O ⧸ Ideal.span {b}) := Fintype.ofFinite (O ⧸ Ideal.span {b})hsum:∑ x, χa ((Ideal.Quotient.factor ⋯) x) * χb ((Ideal.Quotient.factor ⋯) x) * (eisTraceProdChar ShortDraftTrace.breveE breveE_period_coordinates a b ha hb) x = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb)hnorm:↑‖eisEmbedding (a * b)‖ = ↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖⊢ χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) * gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = χa ((Ideal.Quotient.mk (Ideal.span {a})) b) * χb ((Ideal.Quotient.mk (Ideal.span {b})) a) * (gaussSum χa (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates a ha) / ↑‖eisEmbedding a‖) * (gaussSum χb (eisTraceModChar ShortDraftTrace.breveE breveE_period_coordinates b hb) / ↑‖eisEmbedding b‖) All goals completed! 🐙end ConcreteBreveEnamespace FixedRayActiveSetopen scoped BigOperatorsprivate theorem sum_zero_and_units {F : Type*} [Field F] [Fintype F] (f : F → ℂ) : (∑ x : F, f x) = f 0 + ∑ u : Fˣ, f (u : F) := F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∑ x, f x = f 0 + ∑ u, f ↑u classical calc (∑ x : F, f x) = f 0 + ∑ x ∈ (Finset.univ : Finset F).erase 0, f x := F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∑ x, f x = f 0 + ∑ x ∈ univ.erase 0, f x All goals completed! 🐙 _ = f 0 + ∑ x : {x : F // x ≠ 0}, f x := F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ f 0 + ∑ x ∈ univ.erase 0, f x = f 0 + ∑ x, f ↑x F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∑ x ∈ univ.erase 0, f x = ∑ x, f ↑x F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∀ (x : F), x ∈ univ.erase 0 ↔ x ≠ 0 F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂx:F⊢ x ∈ univ.erase 0 ↔ x ≠ 0 All goals completed! 🐙 _ = f 0 + ∑ u : Fˣ, f (u : F) := F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ f 0 + ∑ x, f ↑x = f 0 + ∑ u, f ↑u F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∑ x, f ↑x = ∑ u, f ↑u F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂ⊢ ∀ (x : Fˣ), f ↑x = f ↑(unitsEquivNeZero x) F:Type u_1inst✝¹:Field Finst✝:Fintype Ff:F → ℂu:Fˣ⊢ f ↑u = f ↑(unitsEquivNeZero u) All goals completed! 🐙theorem product_sum_by_active_set {ι : Type*} [Fintype ι] (F : ι → Type*) [∀ i, Field (F i)] [∀ i, Fintype (F i)] (f : ∀ i, F i → ℂ) : (∑ h : ∀ i, F i, ∏ i, f i (h i)) = ∑ A ∈ (Finset.univ : Finset ι).powerset, (∏ i ∈ A, ∑ u : (F i)ˣ, f i (u : F i)) * (∏ i ∈ (Finset.univ : Finset ι) \ A, f i 0) := ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂ⊢ ∑ h, ∏ i, f i (h i) = ∑ A ∈ univ.powerset, (∏ i ∈ A, ∑ u, f i ↑u) * ∏ i ∈ univ \ A, f i 0 classical calc (∑ h : ∀ i, F i, ∏ i, f i (h i)) = ∏ i, ∑ h : F i, f i h := ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂ⊢ ∑ h, ∏ i, f i (h i) = ∏ i, ∑ h, f i h All goals completed! 🐙 _ = ∏ i, ((∑ u : (F i)ˣ, f i (u : F i)) + f i 0) := ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂ⊢ ∏ i, ∑ h, f i h = ∏ i, (∑ u, f i ↑u + f i 0) ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂ⊢ ∀ x ∈ univ, ∑ h, f x h = ∑ u, f x ↑u + f x 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂi:ιa✝:i ∈ univ⊢ ∑ h, f i h = ∑ u, f i ↑u + f i 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)f:(i : ι) → F i → ℂi:ιa✝:i ∈ univ⊢ f i 0 + ∑ u, f i ↑u = ∑ u, f i ↑u + f i 0 All goals completed! 🐙 _ = _ := Finset.prod_add (fun i => ∑ u : (F i)ˣ, f i (u : F i)) (fun i => f i 0) Finset.univtheorem branch_zero_of_local_mask {ι : Type*} [DecidableEq ι] (I A : Finset ι) (scalar dual inactive : ι → ℂ) (i : ι) (hi : i ∈ A) (hzero : dual i = 0) : (∏ k ∈ A, scalar k * dual k) * (∏ k ∈ I \ A, inactive k) = 0 := ι:Type u_1inst✝:DecidableEq ιI:Finset ιA:Finset ιscalar:ι → ℂdual:ι → ℂinactive:ι → ℂi:ιhi:i ∈ Ahzero:dual i = 0⊢ (∏ k ∈ A, scalar k * dual k) * ∏ k ∈ I \ A, inactive k = 0 ι:Type u_1inst✝:DecidableEq ιI:Finset ιA:Finset ιscalar:ι → ℂdual:ι → ℂinactive:ι → ℂi:ιhi:i ∈ Ahzero:dual i = 0hprod:∏ k ∈ A, scalar k * dual k = 0⊢ (∏ k ∈ A, scalar k * dual k) * ∏ k ∈ I \ A, inactive k = 0 All goals completed! 🐙theorem admissible_branch_count {ι : Type*} [Fintype ι] [DecidableEq ι] (j : ι → ℕ) : ((Finset.univ : Finset ι).powerset.filter (fun A => (Finset.univ.filter (fun i => j i ≠ 0)) ⊆ A)).card ≤ 2 ^ Fintype.card ι := ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕ⊢ #({A ∈ univ.powerset | {i | j i ≠ 0} ⊆ A}) ≤ 2 ^ Fintype.card ι calc _ ≤ (Finset.univ : Finset ι).powerset.card := Finset.card_filter_le _ _ _ = 2 ^ Fintype.card ι := ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕ⊢ #univ.powerset = 2 ^ Fintype.card ι All goals completed! 🐙private theorem branch_zero_outside_admissible {ι : Type*} [Fintype ι] [DecidableEq ι] (j : ι → ℕ) (scalar dual inactive : ι → ℂ) (hzero : ∀ i, j i ≠ 0 → inactive i = 0) (A : Finset ι) (hnot : ¬ (Finset.univ.filter (fun i => j i ≠ 0)) ⊆ A) : (∏ i ∈ A, scalar i * dual i) * (∏ i ∈ (Finset.univ : Finset ι) \ A, inactive i) = 0 := ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕscalar:ι → ℂdual:ι → ℂinactive:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → inactive i = 0A:Finset ιhnot:¬{i | j i ≠ 0} ⊆ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, inactive i = 0 ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕscalar:ι → ℂdual:ι → ℂinactive:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → inactive i = 0A:Finset ιhnot:¬{i | j i ≠ 0} ⊆ Ai:ιhiM:i ∈ {i | j i ≠ 0}hiA:i ∉ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, inactive i = 0 ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕscalar:ι → ℂdual:ι → ℂinactive:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → inactive i = 0A:Finset ιhnot:¬{i | j i ≠ 0} ⊆ Ai:ιhiM:i ∈ {i | j i ≠ 0}hiA:i ∉ Ahj:j i ≠ 0⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, inactive i = 0 ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕscalar:ι → ℂdual:ι → ℂinactive:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → inactive i = 0A:Finset ιhnot:¬{i | j i ≠ 0} ⊆ Ai:ιhiM:i ∈ {i | j i ≠ 0}hiA:i ∉ Ahj:j i ≠ 0hi:i ∈ univ \ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, inactive i = 0 ι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιj:ι → ℕscalar:ι → ℂdual:ι → ℂinactive:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → inactive i = 0A:Finset ιhnot:¬{i | j i ≠ 0} ⊆ Ai:ιhiM:i ∈ {i | j i ≠ 0}hiA:i ∉ Ahj:j i ≠ 0hi:i ∈ univ \ Ahprod:∏ k ∈ univ \ A, inactive k = 0⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, inactive i = 0 All goals completed! 🐙theorem assemble_local_A5 {ι : Type*} [Fintype ι] (F : ι → Type*) [∀ i, Field (F i)] [∀ i, Fintype (F i)] (j : ι → ℕ) (f : ∀ i, F i → ℂ) (scalar dual : ι → ℂ) (hzero : ∀ i, j i ≠ 0 → f i 0 = 0) (hactive : ∀ i, (∑ u : (F i)ˣ, f i (u : F i)) = scalar i * dual i) : (∑ h : ∀ i, F i, ∏ i, f i (h i)) = ∑ A ∈ ((Finset.univ : Finset ι).powerset.filter (fun A => (Finset.univ.filter (fun i => j i ≠ 0)) ⊆ A)), (∏ i ∈ A, scalar i * dual i) * (∏ i ∈ (Finset.univ : Finset ι) \ A, f i 0) := ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual i⊢ ∑ h, ∏ i, f i (h i) = ∑ A ∈ univ.powerset with {i | j i ≠ 0} ⊆ A, (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 classical ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual i⊢ ∑ A ∈ univ.powerset, (∏ i ∈ A, ∑ u, f i ↑u) * ∏ i ∈ univ \ A, f i 0 = ∑ A ∈ univ.powerset with {i | j i ≠ 0} ⊆ A, (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual i⊢ ∑ A ∈ univ.powerset, (∏ i ∈ A, ∑ u, f i ↑u) * ∏ i ∈ univ \ A, f i 0 = ∑ A ∈ univ.powerset with {i | j i ≠ 0} ⊆ A, (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 conv_lhs => ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual i| fun A => (∏ i ∈ A, ∑ u, f i ↑u) * ∏ i ∈ univ \ A, f i 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ι| (∏ i ∈ A, ∑ u, f i ↑u) * ∏ i ∈ univ \ A, f i 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ι| (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual i⊢ ∑ A ∈ univ.powerset, (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = ∑ a ∈ univ.powerset, if {i | j i ≠ 0} ⊆ a then (∏ i ∈ a, scalar i * dual i) * ∏ i ∈ univ \ a, f i 0 else 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual i⊢ ∀ x ∈ univ.powerset, (∏ i ∈ x, scalar i * dual i) * ∏ i ∈ univ \ x, f i 0 = if {i | j i ≠ 0} ⊆ x then (∏ i ∈ x, scalar i * dual i) * ∏ i ∈ univ \ x, f i 0 else 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ιhA:A ∈ univ.powerset⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = if {i | j i ≠ 0} ⊆ A then (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 else 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ιhA:A ∈ univ.powersethAdmissible:{i | j i ≠ 0} ⊆ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = if {i | j i ≠ 0} ⊆ A then (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 else 0ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ιhA:A ∈ univ.powersethAdmissible:¬{i | j i ≠ 0} ⊆ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = if {i | j i ≠ 0} ⊆ A then (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 else 0 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ιhA:A ∈ univ.powersethAdmissible:{i | j i ≠ 0} ⊆ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = if {i | j i ≠ 0} ⊆ A then (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 else 0 All goals completed! 🐙 ι:Type u_1inst✝²:Fintype ιF:ι → Type u_2inst✝¹:(i : ι) → Field (F i)inst✝:(i : ι) → Fintype (F i)j:ι → ℕf:(i : ι) → F i → ℂscalar:ι → ℂdual:ι → ℂhzero:∀ (i : ι), j i ≠ 0 → f i 0 = 0hactive:∀ (i : ι), ∑ u, f i ↑u = scalar i * dual ihreplace:∀ (A : Finset ι), ∏ i ∈ A, ∑ u, f i ↑u = ∏ i ∈ A, scalar i * dual iA:Finset ιhA:A ∈ univ.powersethAdmissible:¬{i | j i ≠ 0} ⊆ A⊢ (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 = if {i | j i ≠ 0} ⊆ A then (∏ i ∈ A, scalar i * dual i) * ∏ i ∈ univ \ A, f i 0 else 0 All goals completed! 🐙end FixedRayActiveSetnamespace CubeInversiontheorem cube_index_filter_complex (m : ℕ) : (∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ)) = if m = 1 then 1 else 0 := m:ℕ⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) = if m = 1 then 1 else 0 m:ℕh:(ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta) m = 1 m⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) = if m = 1 then 1 else 0 m:ℕh:∑ i ∈ m.divisors, ArithmeticFunction.moebius i = if m = 1 then 1 else 0⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) = if m = 1 then 1 else 0 All goals completed! 🐙theorem cube_coefficient_filter (m : ℕ) (c W : ℕ → ℂ) (hc : ∀ a b, c (a * b) = c a * c b) : (∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ) * c h * c (m / h) * W m) = if m = 1 then c m * W m else 0 := m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c b⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = if m = 1 then c m * W m else 0 m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = if m = 1 then c m * W m else 0 calc (∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ) * c h * c (m / h) * W m) = (∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ)) * (c m * W m) := m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = (∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h)) * (c m * W m) m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = ∑ i ∈ m.divisors, ↑(ArithmeticFunction.moebius i) * (c m * W m) m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ ∀ x ∈ m.divisors, ↑(ArithmeticFunction.moebius x) * c x * c (m / x) * W m = ↑(ArithmeticFunction.moebius x) * (c m * W m) m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh:ℕhh:h ∈ m.divisors⊢ ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = ↑(ArithmeticFunction.moebius h) * (c m * W m) calc (ArithmeticFunction.moebius h : ℂ) * c h * c (m / h) * W m = (ArithmeticFunction.moebius h : ℂ) * (c h * c (m / h)) * W m := m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh:ℕhh:h ∈ m.divisors⊢ ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = ↑(ArithmeticFunction.moebius h) * (c h * c (m / h)) * W m All goals completed! 🐙 _ = (ArithmeticFunction.moebius h : ℂ) * (c m * W m) := m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh:ℕhh:h ∈ m.divisors⊢ ↑(ArithmeticFunction.moebius h) * (c h * c (m / h)) * W m = ↑(ArithmeticFunction.moebius h) * (c m * W m) m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh:ℕhh:h ∈ m.divisors⊢ ↑(ArithmeticFunction.moebius h) * c m * W m = ↑(ArithmeticFunction.moebius h) * (c m * W m) All goals completed! 🐙 _ = if m = 1 then c m * W m else 0 := m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ (∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h)) * (c m * W m) = if m = 1 then c m * W m else 0 m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c m⊢ (if m = 1 then 1 else 0) * (c m * W m) = if m = 1 then c m * W m else 0 m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh✝:m = 1⊢ 1 * (c m * W m) = c m * W mm:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh✝:¬m = 1⊢ 0 * (c m * W m) = 0 m:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh✝:m = 1⊢ 1 * (c m * W m) = c m * W mm:ℕc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c bheq:∀ h ∈ m.divisors, c h * c (m / h) = c mh✝:¬m = 1⊢ 0 * (c m * W m) = 0 All goals completed! 🐙theorem finite_cube_inversion (S : Finset ℕ) (hS : 1 ∈ S) (c W : ℕ → ℂ) (hc : ∀ a b, c (a * b) = c a * c b) : (∑ m ∈ S, ∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ) * c h * c (m / h) * W m) = c 1 * W 1 := S:Finset ℕhS:1 ∈ Sc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c b⊢ ∑ m ∈ S, ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = c 1 * W 1 simp_rw S:Finset ℕhS:1 ∈ Sc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c b⊢ ∑ m ∈ S, ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W m = c 1 * W 1S:Finset ℕhS:1 ∈ Sc:ℕ → ℂW:ℕ → ℂhc:∀ (a b : ℕ), c (a * b) = c a * c b⊢ (∑ x ∈ S, if x = 1 then c x * W x else 0) = c 1 * W 1] All goals completed! 🐙theorem finite_cube_inversion_with_columns {N : Type*} [DecidableEq N] (columns : Finset N) (S : Finset ℕ) (hS : 1 ∈ S) (a : N → ℂ) (c : ℕ → ℂ) (W : N → ℕ → ℂ) (hc : ∀ x y, c (x * y) = c x * c y) : (∑ n ∈ columns, a n * (∑ m ∈ S, ∑ h ∈ m.divisors, (ArithmeticFunction.moebius h : ℂ) * c h * c (m / h) * W n m)) = ∑ n ∈ columns, a n * (c 1 * W n 1) := N:Type u_1inst✝:DecidableEq Ncolumns:Finset NS:Finset ℕhS:1 ∈ Sa:N → ℂc:ℕ → ℂW:N → ℕ → ℂhc:∀ (x y : ℕ), c (x * y) = c x * c y⊢ ∑ n ∈ columns, a n * ∑ m ∈ S, ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W n m = ∑ n ∈ columns, a n * (c 1 * W n 1) N:Type u_1inst✝:DecidableEq Ncolumns:Finset NS:Finset ℕhS:1 ∈ Sa:N → ℂc:ℕ → ℂW:N → ℕ → ℂhc:∀ (x y : ℕ), c (x * y) = c x * c y⊢ ∀ x ∈ columns, a x * ∑ m ∈ S, ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W x m = a x * (c 1 * W x 1) N:Type u_1inst✝:DecidableEq Ncolumns:Finset NS:Finset ℕhS:1 ∈ Sa:N → ℂc:ℕ → ℂW:N → ℕ → ℂhc:∀ (x y : ℕ), c (x * y) = c x * c yn:Nhn:n ∈ columns⊢ a n * ∑ m ∈ S, ∑ h ∈ m.divisors, ↑(ArithmeticFunction.moebius h) * c h * c (m / h) * W n m = a n * (c 1 * W n 1) All goals completed! 🐙end CubeInversionnamespace ActualEisensteinCubicopen EisensteinEmbedding ConcreteTraceCRT PrimitiveTracenoncomputable def breveGammaMinus1 (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) : ℂ := gaussSum (canonicalSextic P hgood)⁻¹ (hP.symm ▸ eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp) / (‖eisEmbedding p‖ : ℂ)private theorem canonicalSextic_order_six (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (hchar : ringChar (O ⧸ P) ≠ 2) : orderOf (canonicalSextic P hgood) = 6 := P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2⊢ orderOf (canonicalSextic P hgood) = 6 P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2Φ:MulChar (O ⧸ P) O →* MulChar (O ⧸ P) ℂ := ringHomCompHom eisEmbedding⊢ orderOf (canonicalSextic P hgood) = 6 P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2Φ:MulChar (O ⧸ P) O →* MulChar (O ⧸ P) ℂ := ringHomCompHom eisEmbeddinghΦ:Function.Injective ⇑Φ⊢ orderOf (canonicalSextic P hgood) = 6 P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2Φ:MulChar (O ⧸ P) O →* MulChar (O ⧸ P) ℂ := ringHomCompHom eisEmbeddinghΦ:Function.Injective ⇑Φ⊢ orderOf (Φ (sexticChar P hgood)) = 6 All goals completed! 🐙theorem breveGamma1_gammaMinus1 (P : Ideal O) [P.IsMaximal] (hgood : lambda ∉ P) (hchar : ringChar (O ⧸ P) ≠ 2) (p : O) (hP : P = Ideal.span {p}) (hp : p ≠ 0) (hprimary : lambda ^ 2 ∣ p - 1) : breveGamma1 P hgood p hP hp * breveGammaMinus1 P hgood p hP hp = canonicalSextic P hgood (Ideal.Quotient.mk P (-1 : O)) := P:Ideal Oinst✝:P.IsMaximalhgood:lambda ∉ Phchar:ringChar (O ⧸ P) ≠ 2p:OhP:P = Ideal.span {p}hp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1⊢ breveGamma1 P hgood p hP hp * breveGammaMinus1 P hgood p hP hp = (canonicalSextic P hgood) ((Ideal.Quotient.mk P) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgood⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hp⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitive⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0⊢ breveGamma1 (Ideal.span {p}) hgood p ⋯ hp * breveGammaMinus1 (Ideal.span {p}) hgood p ⋯ hp = (canonicalSextic (Ideal.span {p}) hgood) ((Ideal.Quotient.mk (Ideal.span {p})) (-1)) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0⊢ gaussSum χ ψ / s * (gaussSum χ⁻¹ ψ / s) = χ (-1) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ = s ^ 2 * χ (-1) p:Ohp:p ≠ 0hprimary:lambda ^ 2 ∣ p - 1inst✝:(Ideal.span {p}).IsMaximalhgood:lambda ∉ Ideal.span {p}hchar:ringChar (O ⧸ Ideal.span {p}) ≠ 2χ:MulChar (O ⧸ Ideal.span {p}) ℂ := canonicalSextic (Ideal.span {p}) hgoodψ:AddChar (EisensteinEmbedding.O ⧸ Ideal.span {p}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates p hps:ℂ := ↑‖eisEmbedding p‖hψ:ψ.IsPrimitivehχ1:χ ≠ 1hχ6:χ ^ 6 = 1horder:orderOf χ = 6hχ5:χ ^ 5 = χ⁻¹hprod:gaussSum χ ψ * gaussSum χ⁻¹ ψ = χ (-1) * ↑(Fintype.card (O ⧸ Ideal.span {p}))hs:s ^ 2 = ↑(Fintype.card (O ⧸ Ideal.span {p}))hs0:s ≠ 0⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ = ↑(Fintype.card (O ⧸ Ideal.span {p})) * χ (-1) All goals completed! 🐙end ActualEisensteinCubicendend OAI