CubicThetaKubotaSupplement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The elementary supplementary-law calculation used for the Kubota multiplier in DR v3 Remark 5.1.

lemma OAI.CubicFirstMoment.cubicSymbol_periodic_of_nine_and_numerator line 13
Source documentation
The unit and ramified factors need only congruence modulo nine; the primary factor needs congruence modulo the numerator itself.
```
lemma cubicSymbol_periodic_of_nine_and_numerator {a b c : Eisenstein}
    (ha : primary a) (hb : primary b) (h9 : (9:Eisenstein) ∣ a-b)
    (hc : c ∣ a-b) : cubicSymbol a c = cubicSymbol b c := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol
lemma OAI.CubicFirstMoment.cubicThetaKubota_symbol_one line 35
Source documentation
If a primary denominator is one modulo nine and modulo the numerator, all unit, ramified and primary parts of its cubic residue value are one.
```
lemma cubicThetaKubota_symbol_one {D c : Eisenstein} (hD : primary D)
    (h9 : (9:Eisenstein) ∣ D-1) (hc : c ∣ D-1) : cubicSymbol D c = 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol