feat(NumberField/FundamentalCone): generalize the bijection to integral ideals

[xroblot]

This PR is part of the proof of the Analytic Class Number Formula.

---

[github-actions[bot]]

PR summary b7e08e3b9b

Import changes for modified files

Dependency changes

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

Import changes for all files

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

---

Declarations diff

+ card_isPrincipal_dvd_norm_le + exists_unique_preimage_of_mem_integerSet + exists_unitSMul_mem_integerSet + idealSet + idealSetEquiv + idealSetEquivNorm + idealSetEquiv_apply + idealSetEquiv_symm_apply + idealSetMap + idealSetMap_apply + instance : MulAction (torsion K) (integerSet K) + intNorm_idealSetEquiv_apply + integerSet + integerSetEquiv + integerSetEquivNorm + integerSetEquivNorm_apply_fst + integerSetEquiv_apply_fst + integerSetQuotEquivAssociates + integerSetQuotEquivAssociates_apply + integerSetToAssociates + integerSetToAssociates_apply + integerSetToAssociates_eq_iff + integerSetToAssociates_surjective + integerSetTorsionSMul: + integerSetTorsionSMul_stabilizer + mem_idealSet + mem_integerSet + mixedEmbedding_preimageOfMemIntegerSet + ne_zero_of_mem_integerSet + preimageOfMemIntegerSet + preimageOfMemIntegerSet_mixedEmbedding + preimage_of_IdealSetMap + torsion_unitSMul_mem_integerSet - card_isPrincipal_norm_le_mul_torsion - exists_unique_preimage_of_integralPoint - exists_unitSMul_mem_integralPoint - instance : MulAction (torsion K) (integralPoint K) - integralPoint - integralPointEquiv - integralPointEquivNorm - integralPointEquivNorm_apply_fst - integralPointEquiv_apply_fst - integralPointQuotEquivAssociates - integralPointQuotEquivAssociates_apply - integralPointToAssociates - integralPointToAssociates_apply - integralPointToAssociates_eq_iff - integralPointToAssociates_surjective - integralPoint_ne_zero - integralPoint_torsionSMul: - integralPoint_torsionSMul_stabilizer - mem_integralPoint - mixedEmbedding_preimageOfIntegralPoint - preimageOfIntegralPoint - preimageOfIntegralPoint_mixedEmbedding - torsion_unitSMul_mem_integralPoint

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.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build