feat(Algebra/QuadraticAlgebra): quadratic extensions are quadratic algebras

[xroblot]

Relates the construction QuadraticAlgebra R a b to the predicate Algebra.IsQuadraticExtension:

• QuadraticAlgebra.instIsQuadraticExtension: a QuadraticAlgebra is a quadratic extension;
• Algebra.IsQuadraticExtension.exists_algEquiv_quadraticAlgebra: every commutative quadratic
  extension is isomorphic to some QuadraticAlgebra R a b.

---

• depends on: feat(Algebra/QuadraticAlgebra): discriminant and classification #42206
• depends on: feat(Algebra/QuadraticAlgebra): injectivity and surjectivity of lift #42439
• depends on: feat(LinearAlgebra): unimodular elements and completion to a basis #42466

[github-actions]

PR summary 4168244c8d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.QuadraticAlgebra.Basic	1
Mathlib.LinearAlgebra.Unimodular (new file)	1663
Mathlib.Algebra.QuadraticAlgebra.Discr (new file)	1672
Mathlib.Algebra.QuadraticAlgebra.IsQuadraticExtension (new file)	1899

---

Declarations diff (regex)

+ Algebra.aeval_leftMulMatrix_charpoly
+ IsQuadraticExtension.exists_algEquiv_quadraticAlgebra
+ IsQuadraticExtension.sq_eq_trace_smul_sub_norm
+ IsQuadraticExtension.sq_sub_trace_smul_add_norm_eq_zero
+ adjoin_omega_eq_top
+ algEquivDiscrZero
+ algebraMap_discr
+ basis_apply_one
+ basis_apply_zero
+ discr
+ discr_def
+ discr_eq_im_sq_mul_discr
+ discr_eq_im_sq_mul_discr'
+ discr_map
+ exists_basis_apply_zero_eq
+ exists_linearMap_apply_one_eq_one
+ exists_sq_eq_iff_isSquare_discr
+ im_sq_mul_discr
+ instIsQuadraticExtension
+ instIsQuadraticExtensionRat
+ instance {K : Type*} [Field K] {a : K} [Fact (¬ IsSquare a)] :
+ instance {K : Type*} [Field K] {a b : K} [NeZero (2 : K)] [Fact (¬ IsSquare (discr a b))] :
+ isField_iff_not_isSquare_discr
+ isUnit_im_omega_of_algEquiv
+ lift_injective_iff
+ lift_surjective_iff
+ map
+ mapEquiv
+ map_injective
+ map_omega
+ map_relation
+ map_star
+ nonempty_algEquiv_iff
+ nonempty_algEquiv_iff_of_invertible_two
+ nonempty_algEquiv_int_iff
+ norm_map_omega
+ not_isField_of_isSquare_discr
+ range_lift
+ re_smul_add_im_smul
+ smul_omega_sub_eq
+ span_repr_eq_top_iff
+ span_repr_one_eq_top
+ trace_map
+ trace_map_omega

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

• +48 new declarations
• −0 removed declarations

+Algebra.IsQuadraticExtension.exists_algEquiv_quadraticAlgebra
+Algebra.IsQuadraticExtension.sq_eq_trace_smul_sub_norm
+Algebra.IsQuadraticExtension.sq_sub_trace_smul_add_norm_eq_zero
+Algebra.aeval_leftMulMatrix_charpoly
+Matrix.toLinearEquiv.congr_simp
+Module.Basis.span_repr_eq_top_iff
+Module.Basis.span_repr_one_eq_top
+Module.Free.exists_basis_apply_zero_eq
+Module.Free.exists_linearMap_apply_one_eq_one
+QuadraticAlgebra.adjoin_omega_eq_top
+QuadraticAlgebra.algEquivDiscrZero
+QuadraticAlgebra.algebraMap_discr
+QuadraticAlgebra.basis_apply_one
+QuadraticAlgebra.basis_apply_zero
+QuadraticAlgebra.discr
+QuadraticAlgebra.discr_def
+QuadraticAlgebra.discr_eq_im_sq_mul_discr
+QuadraticAlgebra.discr_eq_im_sq_mul_discr'
+QuadraticAlgebra.discr_map
+QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr
+QuadraticAlgebra.im_map_apply
+QuadraticAlgebra.im_sq_mul_discr
+QuadraticAlgebra.instFactForallNeHPowOfNatHAddHMul
+QuadraticAlgebra.instFactForallNeHPowOfNatHAddHMul_1
+QuadraticAlgebra.instIsQuadraticExtension
+QuadraticAlgebra.instIsQuadraticExtensionRat
+QuadraticAlgebra.isField_iff_not_isSquare_discr
+QuadraticAlgebra.isUnit_im_omega_of_algEquiv
+QuadraticAlgebra.lift_injective_iff
+QuadraticAlgebra.lift_surjective_iff
+QuadraticAlgebra.map
+QuadraticAlgebra.map.congr_simp
+QuadraticAlgebra.mapEquiv
+QuadraticAlgebra.mapEquiv_apply
+QuadraticAlgebra.mapEquiv_symm_apply
+QuadraticAlgebra.map_injective
+QuadraticAlgebra.map_omega
+QuadraticAlgebra.map_star
+QuadraticAlgebra.nonempty_algEquiv_iff
+QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two
+QuadraticAlgebra.nonempty_algEquiv_int_iff
+QuadraticAlgebra.norm_map_omega
+QuadraticAlgebra.not_isField_of_isSquare_discr
+QuadraticAlgebra.range_lift
+QuadraticAlgebra.re_map_apply
+QuadraticAlgebra.re_smul_add_im_smul
+QuadraticAlgebra.trace_map
+QuadraticAlgebra.trace_map_omega

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
6991	-1	backward.isDefEq.respectTransparency

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

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

Current commit 4168244c8d
Reference commit 1f8806b67d

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): discriminant and classification #42206
• feat(Algebra/QuadraticAlgebra): injectivity and surjectivity of lift #42439
• feat(LinearAlgebra): unimodular elements and completion to a basis #42466
  By Dependent Issues (🤖). Happy coding!