OAI/NumberTheory/CubicMoment/Estimates/RamifiedPrimaryDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact separation of a nonzero Eisenstein integer into a global unit, a ramified-prime power, and a primary factor.

  1. lemma OAI.CubicFirstMoment.unit_ramified_primary_decomposition line 11