feat(Algebra/QuadraticAlgebra): quadratic orders over ℤ and their fraction ring

[xroblot]

Realize QuadraticAlgebra ℤ a b as an order in QuadraticAlgebra ℚ a b, via the base-change map
algHom: the latter is the localization at the nonzero integers and the fraction ring, and the
former is a domain iff discr a b is not a square.

Prepared with Claude Code 🤖

---

• depends on: [Merged by Bors] - feat(Algebra/QuadraticAlgebra): discriminant and field criterion #42206
• depends on: [Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename map/mapEquiv to changeGenerator #42751
• depends on: feat(Algebra/QuadraticAlgebra): base change of quadratic algebras #42977
• depends on: [Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename Discr to Discriminant #42975

[github-actions]

PR summary 658f1af3aa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.QuadraticAlgebra.Int (new file)	1388

---

Declarations diff (regex)

+ algebraMap_eq
+ algebraMap_im_eq
+ algebraMap_re_eq
+ baseChange
+ baseChange_injective
+ baseChange_omega
+ changeGenerator
+ changeGeneratorEquiv
+ changeGenerator_injective
+ changeGenerator_omega
+ changeGenerator_relation
+ discr_algebraMap
+ discr_changeGenerator
+ discr_intCast
+ exists_nat_smul_mem
+ 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)
+ instance [Fact (¬ IsSquare (discr a b))] : IsDomain (QuadraticAlgebra ℤ a b)
+ instance [h : Fact (¬ IsSquare (discr a b))] : Fact (¬ IsSquare (discr (a : ℚ) (b : ℚ))) := by
+ isDomain_iff
+ isDomain_iff_isField
+ norm_baseChange
+ trace_baseChange
- map_relation

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

• +30 new declarations
• −5 removed declarations

+IsFractionRing.isDomain_iff_isField
+QuadraticAlgebra.Int.algebraMap_eq
+QuadraticAlgebra.Int.algebraMap_im_eq
+QuadraticAlgebra.Int.algebraMap_re_eq
+QuadraticAlgebra.Int.discr_intCast
+QuadraticAlgebra.Int.exists_nat_smul_mem
+QuadraticAlgebra.Int.instAlgebraIntRatCast
+QuadraticAlgebra.Int.instFaithfulSMulIntRatCast
+QuadraticAlgebra.Int.instIsFractionRingIntRatCast
+QuadraticAlgebra.Int.instIsLocalizationIntAlgebraMapSubmonoidNonZeroDivisorsRatCast
+QuadraticAlgebra.Int.instIsScalarTowerIntRatCast
+QuadraticAlgebra.Int.isDomain_iff
+QuadraticAlgebra.baseChange
+QuadraticAlgebra.baseChange_injective
+QuadraticAlgebra.baseChange_omega
+QuadraticAlgebra.changeGenerator
+QuadraticAlgebra.changeGenerator.congr_simp
+QuadraticAlgebra.changeGeneratorEquiv
+QuadraticAlgebra.changeGeneratorEquiv_apply
+QuadraticAlgebra.changeGeneratorEquiv_symm_apply
+QuadraticAlgebra.changeGenerator_injective
+QuadraticAlgebra.changeGenerator_omega
+QuadraticAlgebra.discr_algebraMap
+QuadraticAlgebra.discr_changeGenerator
+QuadraticAlgebra.im_baseChange_apply
+QuadraticAlgebra.im_changeGenerator_apply
-QuadraticAlgebra.im_map_apply
-QuadraticAlgebra.map.congr_simp
-QuadraticAlgebra.mapEquiv_apply
-QuadraticAlgebra.mapEquiv_symm_apply
+QuadraticAlgebra.norm_baseChange
+QuadraticAlgebra.re_baseChange_apply
+QuadraticAlgebra.re_changeGenerator_apply
-QuadraticAlgebra.re_map_apply
+QuadraticAlgebra.trace_baseChange

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4931	1	exposed public sections

Current commit 658f1af3aa
Reference commit caa4dbde35

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-merge-conflicts]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Algebra/QuadraticAlgebra): discriminant and field criterion #42206
• [Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename map/mapEquiv to changeGenerator #42751
• feat(Algebra/QuadraticAlgebra): base change of quadratic algebras #42977
• [Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename Discr to Discriminant #42975
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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