2024-09-23 16:51
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
feat(NumberField/CanonicalEmbedding/FundamentalCone): Prove equivalence with principal ideals (#12333) …
Added NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion