PrimeCoordinateRoles.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The distinguished largest-prime role splits into the actual tuple coordinates with multiplicity one, even in the presence of the selected divisor. No ordering of its prime factors is introduced.

lemma OAI.CubicFirstMoment.prime_tuple_divisor_indicator line 16
theorem OAI.CubicFirstMoment.distinguished_largest_coordinate_roles line 47
Source documentation
A squarefree full product has exactly one distinguished coordinate when its canonical largest prime lies on the distinguished side.
```
theorem distinguished_largest_coordinate_roles [Nonempty ι]
    (f : ι → Eisenstein) (hf : ∀ i, primaryPrime (f i))
    {d : Eisenstein} (hd : primary d) (hs : Squarefree ((∏ i, f i)*d)) (z : ℂ) :
    (if largestPrimeChoice ((∏ i, f i)*d) ∣ ∏ i, f i then z else 0) =
      ∑ i, if largestPrimeChoice ((∏ i, f i)*d) = f i then z else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.largestPrimeChoice