OAI/NumberTheory/Jacobsthal/Analysis/RealCoefficientNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosComplexCurveFactors.realCoefficients line 13
2. theorem OAI.Erdos970.ErdosComplexCurveFactors.coeff_realCoefficients line 16
3. theorem OAI.Erdos970.ErdosComplexCurveFactors.complexify_realCoefficients line 19
4. def OAI.Erdos970.ErdosComplexCurveFactors.RealScalable line 28
5. theorem OAI.Erdos970.ErdosComplexCurveFactors.normalized_conjugate_eq line 31
6. theorem OAI.Erdos970.ErdosComplexCurveFactors.realScalable_of_dvd_conjugate line 42
7. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonreal_not_dvd_conjugate line 58