CubicThetaKubotaAlternative.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The alternative (b/d) expression for the actual cubic Kubota multiplier on the principal congruence group.

lemma OAI.CubicFirstMoment.cubicThetaPrincipalGroup_offDiagonal line 12
lemma OAI.CubicFirstMoment.cubicThetaPrincipalGroup_det line 24
lemma OAI.CubicFirstMoment.cubicThetaKubota_column_switch line 28
theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_alternative line 57
Source documentation
DR v3 (5.5), derived from the supplementary laws and determinant.
```
theorem cubicThetaKubotaValue_alternative (g : cubicThetaPrincipalGroup) :
    cubicThetaKubotaValue g =
      if g.val 1 0 = 0 then 1 else cubicSymbol (g.val 1 1) (g.val 0 1) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaPrincipalGroup, OAI.CubicFirstMoment.cubicThetaKubotaValue, OAI.CubicFirstMoment.cubicSymbol