OAI/NumberTheory/PiExponent/LocalAlgebra/ParameterResidueField.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponent.ParameterResidueField.residue_finiteline 10 - abbrev
OAI.PiExponent.ParameterResidueField.parameterChartConstantsline 17 - theorem
OAI.PiExponent.ParameterResidueField.parameterChartConstants_towerline 23 - theorem
OAI.PiExponent.ParameterResidueField.parameter_residue_finiteline 33 - theorem
OAI.PiExponent.ParameterResidueField.parameter_residue_integralline 55