feat(CanonicalEmbedding/FundamentalCone): Prove equivalence with principal ideals

[xroblot]

---

• [ ] depends on: #12268
• [ ] depends on: #12780

[github-actions[bot]]

PR summary fda02a2d54

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone	2231	2232	+1 (+0.04%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone	1

---

Declarations diff

+ card_isPrincipal_norm_eq_mul_torsion + card_isPrincipal_norm_le_mul_torsion + integralPointEquiv + integralPointEquivNorm + integralPointEquivNorm_apply_fst + integralPointEquiv_apply_fst + integralPointQuotEquivAssociates + integralPointQuotEquivAssociates_apply + integralPointToAssociates + integralPointToAssociates_apply + integralPointToAssociates_eq_iff + integralPointToAssociates_surjective + integralPoint_torsionSMul_stabilizer

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12268~~
• ~~leanprover-community/mathlib4#12780~~
• ~~leanprover-community/mathlib4#16921~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

:v: xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style