WIP: splitting of primes in quadratic fields

[xroblot]

Draft PR opened to get CI to build the branch. Not for review.

[github-actions]

PR summary 1a0a897245

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.FundamentalDiscriminant	1
6 files Mathlib.Algebra.QuadraticAlgebra.AlgHom Mathlib.Algebra.QuadraticAlgebra.Basic Mathlib.Algebra.QuadraticAlgebra.Discr Mathlib.Algebra.QuadraticAlgebra.Discriminant Mathlib.Algebra.QuadraticAlgebra.IsQuadraticExtension Mathlib.Algebra.QuadraticAlgebra.NormDeterminant	2
Mathlib.Algebra.QuadraticAlgebra.Int (new file)	1852
Mathlib.RingTheory.QuadraticAlgebra (new file)	2019
Mathlib.NumberTheory.NumberField.QuadraticField.Basic (new file)	2988
Mathlib.Sandbox (new file)	3491
Mathlib.Misc (new file)	3492

---

Declarations diff (regex)

+ Algebra.discr_quadraticAlgebra
+ Algebra.norm_quadraticAlgebra_apply
+ Algebra.trace_quadraticAlgebra_apply
+ Finite.isField_iff_isDomain
+ Ideal.isPrime_iff_isMaximal_of_finite_quotient
+ IsDedekindDomain.of_ringEquiv
+ IsFundamentalDiscr.eq_one_of_isSquare
+ LinearEquiv.length_eq'
+ Module.length_eq_of_equiv_equiv
+ NumberField.dvd_discr_iff_exists_two_le_ramificationIdx
+ NumberField.of_isQuadraticExtension
+ QuadraticAlgebra.discr_intCast'
+ QuadraticAlgebra.minpoly_omega
+ QuadraticAlgebra.omega_notMem_range_algebraMap
+ QuadraticAlgebra.polynomial_discr_eq_discr
+ Squarefree.isUnit_of_pow
+ ZMod.neZero_two_of_ne_two
+ _root_.Int.IsFundamentalDiscr.discr_ediv_four_emod_four
+ adjoin_eq_restrictScalars_adjoin_of_surjective
+ adjoin_integralGen_eq_top
+ algEquivDualNumber
+ algEquivDualNumberOfDiscrZero
+ algEquivIntegralClosure
+ algEquivOfRingEquiv
+ algEquivProdOfDiscrSq
+ algEquivProdOfIsUnit
+ algebraMap_eq
+ algebraMap_im_eq
+ algebraMap_re_eq
+ baseChange
+ baseChange_injective
+ baseChange_omega
+ comap_isPrime_iff
+ discr_algebraMap
+ discr_eq_im_sq_mul_discr'
+ discr_eq_quadraticAlgebra_discr
+ discr_half
+ discr_intCast
+ discr_ne_one
+ discr_quadraticAlgebra
+ discr_quadraticAlgebra_eq
+ discr_sqrtd
+ discrim_eq_polynomial_discr
+ discrim_minpoly_integralGen
+ embeddingEquiv
+ embeddingEquiv_symm_apply
+ embeddingEquiv_symm_apply_omega
+ equivOfEq
+ exists_discr_mul_im_sq_eq
+ exists_nat_smul_mem
+ exists_sq_eq_discr
+ exists_unsaturated_of_sq_mul
+ exponent_integralGen
+ four_mul_norm_eq
+ four_mul_norm_smul_one_add_omega
+ im_inv_smul_notMem_range
+ inertiaDeg_comap_eq
+ inertiaDeg_le_finrank'
+ inertiaDeg_map_eq
+ inertiaDeg_of_dvd_discr
+ inertiaDeg_of_isSquare
+ inertiaDeg_of_not_isSquare
+ inertiaDeg_primesOverSpanEquivMonicFactorsMod_apply
+ inertiaDeg_two_of_discr_emod_eight
+ inertiaDeg_two_of_discr_emod_eight_one
+ instance :
+ instance : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
+ instance : Algebra.IsQuadraticExtension ℤ (𝓞 K)
+ instance : FaithfulSMul (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
+ instance : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) := by
+ instance : IsScalarTower ℤ (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
+ instance {R : Type*} {a b : R} [Finite R] : Finite (QuadraticAlgebra R a b)
+ integralGen
+ irreducible_monicFactorsMod
+ irreducible_quadratic_of_not_isSquare_discrim
+ isDedekindDomain_quadraticAlgebra
+ isDomain_iff
+ isDomain_iff_isField
+ isField_iff_forall_sq_ne
+ isField_of_forall_sq_ne
+ isFundamentalDiscr_discr
+ isIntegralClosure_iff_forall_prime
+ isIntegral_iff
+ isIntegral_inv_smul_of_dvd
+ isIntegral_omega
+ isIntegral_star
+ isIntegrallyClosed_iff
+ isReal_embeddingEquiv_symm_iff
+ isTotallyComplex_iff_discr_neg
+ isTotallyReal_iff_discr_pos
+ map_isPrime_iff
+ mem_map_algebraMap_iff
+ mem_monicFactorsMod_iff
+ mem_range_of_dvd_im
+ minpoly_integralGen
+ mk_surjective
+ monicFactorsMod_dvd_map_minpoly
+ monic_minpoly_integralGen
+ monic_monicFactorsMod
+ natDegree_minpoly_integralGen
+ ncard_primesOver_le_finrank'
+ ncard_primesOver_mul_ramificationIdx_mul_inertiaDeg
+ ncard_primesOver_of_dvd_discr
+ ncard_primesOver_of_isSquare
+ ncard_primesOver_of_not_isSquare
+ ncard_primesOver_two_of_discr_emod_eight_five
+ ncard_primesOver_two_of_discr_emod_eight_one
+ nonempty_algEquiv_iff_discr_eq
+ nonempty_algEquiv_quadraticAlgebra_discr
+ nonempty_algEquiv_ringOfIntegers
+ norm_baseChange
+ norm_mem_range_of_isIntegral
+ norm_smul
+ normalizedFactors_quadratic_of_discrim_eq_sq
+ normalizedFactors_quadratic_of_not_isSquare_discrim
+ not_dvd_exponent_integralGen
+ not_isField_of_exists_sq_eq
+ not_isSquare_discr
+ not_isSquare_intCast
+ not_two_dvd_iff_odd
+ quadraticAlgebraAlgEquiv
+ quadratic_eq_mul_of_discrim_eq_sq
+ ramificationIdx_comap_eq'
+ ramificationIdx_le_finrank'
+ ramificationIdx_map_eq'
+ ramificationIdx_of_dvd_discr
+ ramificationIdx_of_isSquare
+ ramificationIdx_of_not_isSquare
+ ramificationIdx_primesOverSpanEquivMonicFactorsMod_apply
+ ramificationIdx_two_of_discr_emod_eight_five
+ ramificationIdx_two_of_discr_emod_eight_one
+ re_mem_range_of_im_mem_range
+ saturated_iff_of_odd
+ saturated_two_iff
+ trace_baseChange
+ trace_mem_range_of_isIntegral
+ trace_smul_one_add_omega
++ discr_emod_four
++ isIntegralClosure_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (4.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5080	4

Current commit 1a0a897245
Reference commit c58b47adb3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).