feat(Algebra/QuadraticAlgebra): maximal quadratic orders over ℤ

[xroblot]

For a b : ℤ, the order QuadraticAlgebra ℤ a b is the integral closure of ℤ in QuadraticAlgebra ℚ a b if and only if discr a b is a fundamental discriminant. This PR proves that, and gives the resulting isomorphism with integralClosure ℤ (QuadraticAlgebra ℚ a b).

It also adds a few supporting lemmas to existing files.

Prepared with Claude Code 🤖

---

• depends on: feat(Algebra/QuadraticAlgebra): classify quadratic algebras by their discriminant #42708
• depends on: feat(Algebra/QuadraticAlgebra): quadratic orders over ℤ and their fraction ring #42711
• depends on: [Merged by Bors] - feat(NumberTheory/FundamentalDiscriminant): fundamental discriminants #42814

[github-actions]

PR summary 1daa93f8a6

Import changes exceeding 2%

%	File
+22.12%	Mathlib.Algebra.QuadraticAlgebra.Discriminant

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.QuadraticAlgebra.Discriminant	1379	1684	+305 (+22.12%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.QuadraticAlgebra.Discr Mathlib.Algebra.QuadraticAlgebra.Discriminant	305
Mathlib.NumberTheory.FundamentalDiscriminant (new file)	1246
Mathlib.Algebra.QuadraticAlgebra.AlgHom (new file)	1682
Mathlib.Algebra.QuadraticAlgebra.Int (new file)	1791

---

Declarations diff (regex)

+ IsCoprime.dvd_mul_left_iff
+ IsCoprime.dvd_mul_right_iff
+ IsFundamentalDiscr
+ IsFundamentalDiscr.emod_four_eq_zero_or_one
+ IsFundamentalDiscr.ne_zero
+ _root_.Odd.isCoprime_two
+ algEquivDiscrZero
+ algEquivIntegralClosure
+ algHom_star
+ algebraMap_eq
+ algebraMap_im_eq
+ algebraMap_re_eq
+ baseChange
+ baseChange_injective
+ baseChange_omega
+ basis_apply_one
+ basis_apply_zero
+ det_toMatrix_algHom
+ discr_algebraMap
+ discr_emod_four
+ discr_eq_im_sq_mul_discr
+ discr_eq_im_sq_mul_discr'
+ discr_intCast
+ exists_discr_mul_im_sq_eq
+ exists_nat_smul_mem
+ exists_unsaturated_of_sq_mul
+ forall_prime_iff_two_and_odd
+ four_mul_norm_eq
+ four_mul_norm_smul_one_add_omega
+ im_inv_smul_notMem_range
+ im_sq_mul_discr
+ instance :
+ instance : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
+ 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)
+ isDomain_iff
+ isDomain_iff_isField
+ isFundamentalDiscr_def
+ isFundamentalDiscr_four_mul
+ isFundamentalDiscr_four_mul_add_one
+ isFundamentalDiscr_iff_forall_prime
+ isFundamentalDiscr_iff_squarefree
+ isIntegralClosure_iff_forall_prime
+ isIntegral_iff
+ isIntegral_inv_smul_of_dvd
+ isIntegral_omega
+ isIntegral_star
+ isRegular_im_omega_iff_injective
+ isUnit_im_omega_of_algEquiv
+ mem_range_of_dvd_im
+ nonempty_algEquiv_iff
+ nonempty_algEquiv_iff_of_invertible_two
+ nonempty_algEquiv_int_iff
+ norm_algHom
+ norm_algHom_omega
+ norm_baseChange
+ norm_mem_range_of_isIntegral
+ norm_smul
+ not_two_dvd_iff_odd
+ re_mem_range_of_im_mem_range
+ re_smul_add_im_smul
+ saturated_iff_of_odd
+ saturated_two_iff
+ smul_omega_sub_eq
+ squarefree_iff_prime_sq_not_dvd
+ toMatrix_algHom
+ trace_algHom
+ trace_algHom_omega
+ trace_baseChange
+ trace_mem_range_of_isIntegral
+ trace_smul_one_add_omega
++ 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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 1daa93f).

• +75 new declarations
• −0 removed declarations

+Int.IsFundamentalDiscr
+Int.IsFundamentalDiscr.emod_four_eq_zero_or_one
+Int.IsFundamentalDiscr.ne_zero
+Int.isFundamentalDiscr_def
+Int.isFundamentalDiscr_four_mul
+Int.isFundamentalDiscr_four_mul_add_one
+Int.isFundamentalDiscr_iff_forall_prime
+Int.isFundamentalDiscr_iff_squarefree
+Int.not_two_dvd_iff_odd
+Int.squarefree_iff_prime_sq_not_dvd
+IsCoprime.dvd_mul_left_iff
+IsCoprime.dvd_mul_right_iff
+IsFractionRing.isDomain_iff_isField
+Nat.forall_prime_iff_two_and_odd
+Odd.isCoprime_two
+QuadraticAlgebra.Int.algEquivIntegralClosure
+QuadraticAlgebra.Int.algebraMap_eq
+QuadraticAlgebra.Int.algebraMap_im_eq
+QuadraticAlgebra.Int.algebraMap_re_eq
+QuadraticAlgebra.Int.discr_intCast
+QuadraticAlgebra.Int.exists_discr_mul_im_sq_eq
+QuadraticAlgebra.Int.exists_nat_smul_mem
+QuadraticAlgebra.Int.exists_unsaturated_of_sq_mul
+QuadraticAlgebra.Int.four_mul_norm_smul_one_add_omega
+QuadraticAlgebra.Int.im_inv_smul_notMem_range
+QuadraticAlgebra.Int.instAlgebraIntRatCast
+QuadraticAlgebra.Int.instFaithfulSMulIntRatCast
+QuadraticAlgebra.Int.instIsFractionRingIntRatCast
+QuadraticAlgebra.Int.instIsLocalizationIntAlgebraMapSubmonoidNonZeroDivisorsRatCast
+QuadraticAlgebra.Int.instIsScalarTowerIntRatCast
+QuadraticAlgebra.Int.isDomain_iff
+QuadraticAlgebra.Int.isIntegralClosure_iff
+QuadraticAlgebra.Int.isIntegralClosure_iff_forall_prime
+QuadraticAlgebra.Int.isIntegral_iff
+QuadraticAlgebra.Int.isIntegral_inv_smul_of_dvd
+QuadraticAlgebra.Int.isIntegral_omega
+QuadraticAlgebra.Int.isIntegral_star
+QuadraticAlgebra.Int.mem_range_of_dvd_im
+QuadraticAlgebra.Int.norm_mem_range_of_isIntegral
+QuadraticAlgebra.Int.re_mem_range_of_im_mem_range
+QuadraticAlgebra.Int.saturated_iff_of_odd
+QuadraticAlgebra.Int.saturated_two_iff
+QuadraticAlgebra.Int.trace_mem_range_of_isIntegral
+QuadraticAlgebra.Int.trace_smul_one_add_omega
+QuadraticAlgebra.algEquivDiscrZero
+QuadraticAlgebra.algHom_star
+QuadraticAlgebra.baseChange
+QuadraticAlgebra.baseChange_injective
+QuadraticAlgebra.baseChange_omega
+QuadraticAlgebra.basis_apply_one
+QuadraticAlgebra.basis_apply_zero
+QuadraticAlgebra.det_toMatrix_algHom
+QuadraticAlgebra.discr_algebraMap
+QuadraticAlgebra.discr_emod_four
+QuadraticAlgebra.discr_eq_im_sq_mul_discr
+QuadraticAlgebra.discr_eq_im_sq_mul_discr'
+QuadraticAlgebra.four_mul_norm_eq
+QuadraticAlgebra.im_baseChange_apply
+QuadraticAlgebra.im_sq_mul_discr
+QuadraticAlgebra.isRegular_im_omega_iff_injective
+QuadraticAlgebra.isUnit_im_omega_of_algEquiv
+QuadraticAlgebra.nonempty_algEquiv_iff
+QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two
+QuadraticAlgebra.nonempty_algEquiv_int_iff
+QuadraticAlgebra.norm_algHom
+QuadraticAlgebra.norm_algHom_omega
+QuadraticAlgebra.norm_baseChange
+QuadraticAlgebra.norm_smul
+QuadraticAlgebra.re_baseChange_apply
+QuadraticAlgebra.re_smul_add_im_smul
+QuadraticAlgebra.toMatrix_algHom
+QuadraticAlgebra.trace_algHom
+QuadraticAlgebra.trace_algHom_omega
+QuadraticAlgebra.trace_baseChange
+isIntegralClosure_iff

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4970	3	exposed public sections

Current commit 1daa93f8a6
Reference commit 8b36e86753

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.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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra/QuadraticAlgebra): classify quadratic algebras by their discriminant #42708
• feat(Algebra/QuadraticAlgebra): quadratic orders over ℤ and their fraction ring #42711
• [Merged by Bors] - feat(NumberTheory/FundamentalDiscriminant): fundamental discriminants #42814
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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