OAI/NumberTheory/DukePrimeDegree/Arithmetic/ZeroPropagation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Propagating a zero to the normal closure

Cyclic factorization gives nonnegative upper bounds for the fixed-field multiplicities. Cyclic induction then shows that a zero of any fixed field forces a zero of the full extension. This avoids an assumption of holomorphy for a general Artin quotient.

  1. theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_nonneg line 28
  2. theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_eq_zero_of_cyclic line 33
  3. theorem OAI.DukePrimeDegree.extension_multiplicity_pos_of_fixedField_pos line 46