feat(NumberField): discriminant in disjoint extensions

[xroblot]

We prove the following results:

• If K₁ and K₂ are linear disjoint number fields with coprime different ideals, then

(discr L).natAbs = (discr K₁).natAbs ^ Module.finrank ℚ K₂ * (discr K₂).natAbs ^ Module.finrank ℚ K₁ 

where L = K₁K₂.

• If K₁ and K₂ are number fields with coprime discriminant and K₁/ℚ Galois, then K₁ and K₂ are linear disjoint.

---

• depends on: feat(NumberTheory): basic results about discriminants in an extension #29940
• depends on: feat(DedekindDomain): lift a basis in a disjoint extension when the different ideals are coprime #29885
• depends on: [Merged by Bors] - feat(IntermediateField/LinearDisjoint): Two fields are linearly disjoint over K iff their intersection is K in the Galois case #27273

[github-actions]

PR summary 5f779bef9d

Import changes exceeding 2%

%	File
+34.41%	Mathlib.NumberTheory.NumberField.Discriminant.Different
+14.55%	Mathlib.RingTheory.FractionalIdeal.Extended

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.Discriminant.Different	2299	3090	+791 (+34.41%)
Mathlib.RingTheory.FractionalIdeal.Extended	1361	1559	+198 (+14.55%)
Mathlib.RingTheory.Ideal.Norm.RelNorm	1993	2024	+31 (+1.56%)
Mathlib.FieldTheory.LinearDisjoint	2034	2058	+24 (+1.18%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.DedekindDomain.Different	1
Mathlib.FieldTheory.LinearDisjoint	24
Mathlib.RingTheory.Ideal.Norm.RelNorm	31
Mathlib.RingTheory.FractionalIdeal.Extended	198
Mathlib.NumberTheory.NumberField.Discriminant.Different	791
Mathlib.RingTheory.DedekindDomain.LinearDisjoint (new file)	2313

---

Declarations diff

+ FractionalIdeal.differentIdeal_dvd_map_differentIdeal
+ FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime
+ FractionalIdeal.differentIdeal_eq_map_differentIdeal
+ FractionalIdeal.inv_le_inv_iff
+ FractionalIdeal.map_differentIdeal_dvd_differentIdeal
+ IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal
+ IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal
+ Module.Basis.ofIsCoprimeDifferentIdeal
+ Module.Basis.ofIsCoprimeDifferentIdeal_apply
+ Module.Basis.ofIsCoprimeDifferentIdeal_aux
+ Module.Basis.traceDual
+ Module.Basis.traceDual_def
+ Module.Basis.traceDual_eq_iff
+ Module.Basis.traceDual_inj
+ Module.Basis.traceDual_injective
+ Module.Basis.traceDual_involutive
+ Module.Basis.traceDual_powerBasis_eq
+ Module.Basis.traceDual_repr_apply
+ Module.Basis.traceDual_traceDual
+ Module.Basis.trace_mul_traceDual
+ Module.Basis.trace_traceDual_mul
+ Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint
+ Submodule.traceDual_le_span_map_traceDual
+ _root_.PowerBasis.ofAdjoinEqTop'
+ _root_.PowerBasis.ofAdjoinEqTop'_dim
+ _root_.PowerBasis.ofAdjoinEqTop'_gen
+ absNorm_algebraMap
+ absNorm_differentIdeal
+ absNorm_relNorm
+ algEquiv_commutes
+ algHom_commutes
+ coe_extendedHomₐ_eq_span
+ differentIdeal_eq_differentIdeal_mul_differentIdeal
+ discr_dvd_discr
+ discr_eq_discr_pow_mul_discr_pow
+ discr_mem_differentIdeal
+ dualBasis_eq_iff
+ dual_eq_dual_mul_dual
+ exists_maximal_ideal_liesOver_of_isIntegral
+ exists_relNorm_eq_pow_of_isPrime
+ extendedHomₐ_coeIdeal_eq_map
+ extendedHomₐ_eq_zero_iff
+ extended_coeIdeal_eq_map
+ extended_eq_zero_iff
+ extended_le_one_of_le_one
+ extended_ne_zero
+ iff_inf_eq_bot
+ instance (B : Type*) [CommRing B] [IsDomain A] [Algebra A B] [NoZeroSMulDivisors A B]
+ isCoprime_differentIdeal_of_isCoprime_discr
+ linearDisjoint_of_isGalois_isCoprime_discr
+ map_injective_of_injective'
+ natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow
+ ne_zero_of_mem_normalizedFactors
+ of_inf_eq_bot
+ one_le_extended_of_one_le
+ relNorm_eq_pow_of_isMaximal
+ relNorm_eq_pow_of_isPrime_isGalois
+ relNorm_int
+ restrictRestrictAlgEquivMapHom
+ restrictRestrictAlgEquivMapHom_apply
+ restrictRestrictAlgEquivMapHom_injective
+ restrictRestrictAlgEquivMapHom_surjective
+ restrictScalars_inj
+ sup
+ traceDual_span_of_basis
+ under_ne_bot
- FixedPoints.mem_intermediateField_iff
- NumberField.absNorm_differentIdeal
- NumberField.discr_mem_differentIdeal

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.

---

Increase in tech debt: (relative, absolute) = (2.00, 0.50)

Current number	Change	Type
4	2	maxHeartBeats modifications

Current commit efd75e14d8
Reference commit 5f779bef9d

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(NumberTheory): basic results about discriminants in an extension #29940
• feat(DedekindDomain): lift a basis in a disjoint extension when the different ideals are coprime #29885
• [Merged by Bors] - feat(IntermediateField/LinearDisjoint): Two fields are linearly disjoint over K iff their intersection is K in the Galois case #27273
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.