[Merged by Bors] - feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras by Nebula691 · Pull Request #27511 · leanprover-community/mathlib4

Nebula691 · 2025-07-26T15:28:22Z

Discussed in #Is there code for X? > Z[(1+sqrt(1+4k))/2] @ 💬

Co-authored-by: Edison Xie [email protected]
Co-authored-by: Kenny Lau [email protected]

github-actions · 2025-07-26T15:29:31Z

PR summary 4a2cfa2512

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.QuadraticAlgebra` (new file)	1273

Declarations diff

+ QuadraticAlgebra
+ algebraMap_eq
+ algebraMap_injective
+ basis
+ basis_repr_apply
+ coe
+ coe_add
+ coe_algebraMap
+ coe_inj
+ coe_injective
+ coe_intCast
+ coe_mul
+ coe_mul_eq_smul
+ coe_natCast
+ coe_neg
+ coe_ofNat
+ coe_one
+ coe_pow
+ coe_smul
+ coe_sub
+ coe_zero
+ equivProd
+ finrank_eq_two
+ im_add
+ im_coe
+ im_intCast
+ im_mul
+ im_natCast
+ im_neg
+ im_ofNat
+ im_one
+ im_smul
+ im_sub
+ im_zero
+ imₗ
+ instCommRing
+ instCommSemiring
+ instNonAssocSemiring
+ instNonUnitalNonAssocSemiring
+ instance : Add (QuadraticAlgebra R a b)
+ instance : AddCommGroupWithOne (QuadraticAlgebra R a b)
+ instance : AddCommMonoidWithOne (QuadraticAlgebra R a b)
+ instance : Coe R (QuadraticAlgebra R a b) := ⟨coe⟩
+ instance : Inhabited (QuadraticAlgebra R a b) := ⟨0⟩
+ instance : Module.Finite R (QuadraticAlgebra R a b) := .of_basis (basis a b)
+ instance : Module.Free R (QuadraticAlgebra R a b) := .of_basis (basis a b)
+ instance : Mul (QuadraticAlgebra R a b)
+ instance : Neg (QuadraticAlgebra R a b) where neg z := ⟨-z.re, -z.im⟩
+ instance : One (QuadraticAlgebra R a b) := ⟨⟨1, 0⟩⟩
+ instance : SMul S (QuadraticAlgebra R a b) where smul s z := ⟨s • z.re, s • z.im⟩
+ instance : Zero (QuadraticAlgebra R a b) := ⟨⟨0, 0⟩⟩
+ instance [AddCommGroup R] : AddCommGroup (QuadraticAlgebra R a b)
+ instance [AddCommMonoid R] : AddCommMonoid (QuadraticAlgebra R a b) := fast_instance% by
+ instance [AddGroup R] : AddGroup (QuadraticAlgebra R a b) := fast_instance% by
+ instance [AddMonoid R] : AddMonoid (QuadraticAlgebra R a b) := fast_instance% by
+ instance [CommSemiring S] [CommSemiring R] [Algebra S R] :
+ instance [Monoid S] [AddMonoid R] [DistribMulAction S R] :
+ instance [Monoid S] [MulAction S R] : MulAction S (QuadraticAlgebra R a b)
+ instance [Nontrivial R] : Nontrivial (QuadraticAlgebra R a b) := (equivProd a b).nontrivial
+ instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticAlgebra R a b)
+ instance [SMul Sᵐᵒᵖ R] [IsCentralScalar S R] : IsCentralScalar S (QuadraticAlgebra R a b)
+ instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticAlgebra R a b)
+ instance [Semiring S] [AddCommMonoid R] [Module S R] : Module S (QuadraticAlgebra R a b)
+ instance [Sub R] : Sub (QuadraticAlgebra R a b)
+ instance [Subsingleton R] : Subsingleton (QuadraticAlgebra R a b) := (equivProd a b).subsingleton
+ instance [Zero S] [SMulWithZero S R] [NoZeroSMulDivisors S R] :
+ linearEquivTuple
+ linearEquivTuple_apply
+ linearEquivTuple_symm_apply
+ mk_add_mk
+ mk_eta
+ mk_mul_mk
+ mk_sub_mk
+ mul_coe_eq_smul
+ neg_mk
+ rank_eq_two
+ re_add
+ re_coe
+ re_intCast
+ re_mul
+ re_natCast
+ re_neg
+ re_ofNat
+ re_one
+ re_smul
+ re_sub
+ re_zero
+ reₗ
+ smul_coe
+ smul_mk

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.

No changes to technical debt.

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

kckennylau

Thanks!

kckennylau · 2025-07-26T20:51:04Z

+@[simp]
+theorem equivTuple_apply {R : Type*} (a b : R) (z : QuadraticAlgebra R a b) :
+    equivTuple a b z = ![z.re, z.im] := rfl


Does the simpNF linter not complain? Also, a and b can be implicit.

it didn't, and making a and b implicit will break the theorems after it then it would ask me to specify which a and b am I using

Co-authored-by: Kenny Lau <[email protected]>

…91/mathlib4 into jiayang/QuadraticAlgebra

eric-wieser

This looks great to me now, thanks!

Co-authored-by: Eric Wieser <[email protected]>

YaelDillies · 2025-09-02T13:30:07Z

There is now plenty of evidence that my original kneejerk reaction was misguided and that we should indeed have this two-fields structure in mathlib.

My reasoning is that this is the minimal first step to unifying Complex and GaussianInt, and that further steps (such as using AdjoinRoot instead of an ad hoc structure) can be taken later (eg once Polynomial has been made computable).

riccardobrasca

LGTM, thanks!

riccardobrasca · 2025-09-03T00:49:02Z

+
+end Neg
+
+section AddGroup


Not super important, but in the section AddGroup there is no mention of any AddGroup.

Co-authored-by: Eric Wieser <[email protected]>

riccardobrasca · 2025-09-05T19:23:37Z

bors merge

…as (#27511) Discussed in [#Is there code for X? > Z[(1+sqrt(1+4k))/2] @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635) Co-authored-by: Edison Xie <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Whysoserioushah <[email protected]> Co-authored-by: Whysoserioushah <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: hongjiayang1 <[email protected]>

mathlib-bors · 2025-09-05T19:37:51Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…as (leanprover-community#27511) Discussed in [#Is there code for X? > Z&leanprover-community#91;(1+sqrt(1+4k))/2&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635) Co-authored-by: Edison Xie <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Whysoserioushah <[email protected]> Co-authored-by: Whysoserioushah <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: hongjiayang1 <[email protected]>

hongjiayang1 added 2 commits July 18, 2025 20:32

for now

80c5cfe

fill in sorrys

cb0b431

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Jul 26, 2025

Whysoserioushah added 3 commits July 26, 2025 16:48

Merge branch 'master' into jiayang/QuadraticAlgebra

5fea4cb

golf proof, add stuff and shake

e8de464

update Mathlib.lean

e29f99f

Nebula691 changed the title ~~Jiayang/quadratic algebra~~ feat(Algebra/QuadraticAlgebra) : Define Quadratic Algebra Jul 26, 2025

Whysoserioushah requested review from eric-wieser, kbuzzard and kckennylau July 26, 2025 16:34

complete docstring

94737d6

Whysoserioushah mentioned this pull request Jul 26, 2025

feat(Algebra): Quadratic Algebra #25223

Closed

kckennylau suggested changes Jul 26, 2025

View reviewed changes

Whysoserioushah and others added 9 commits July 26, 2025 22:14

Update Mathlib/Algebra/QuadraticAlgebra.lean

9603682

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

ebceaa9

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

28a347f

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

a1aeb5b

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

006be5b

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

dc1145e

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

12da698

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

3c983f7

Co-authored-by: Kenny Lau <[email protected]>

Update Mathlib/Algebra/QuadraticAlgebra.lean

9fde7dd

Co-authored-by: Kenny Lau <[email protected]>

eric-wieser reviewed Jul 27, 2025

View reviewed changes

Comment thread Mathlib/Algebra/QuadraticAlgebra.lean Outdated

Whysoserioushah and others added 5 commits July 27, 2025 20:13

kenny suggestion

b610c66

Update Mathlib/Algebra/QuadraticAlgebra.lean

2c8826d

Co-authored-by: Kenny Lau <[email protected]>

fix kenny suggestion 2

00366e6

fix docstring

bb3b4c0

use Coe instead of CoeTC

c91e042

eric-wieser and others added 3 commits September 1, 2025 00:52

Whitespace fixes

3694eed

add nonunitalnonassoc and remove non-necessary stuff

692a785

Merge branch 'jiayang/QuadraticAlgebra' of https://github.com/Nebula6…

ad3cb65

…91/mathlib4 into jiayang/QuadraticAlgebra

eric-wieser reviewed Sep 1, 2025

View reviewed changes

Comment thread Mathlib/Algebra/QuadraticAlgebra.lean

Whysoserioushah added 2 commits September 1, 2025 08:08

generalise lemmas

0c2e1de

split addcommmonoid

215ecdb

eric-wieser reviewed Sep 1, 2025

View reviewed changes

Comment thread Mathlib/Algebra/QuadraticAlgebra.lean Outdated

eric-wieser approved these changes Sep 1, 2025

View reviewed changes

Comment thread Mathlib/Algebra/QuadraticAlgebra.lean Outdated

Whysoserioushah and others added 4 commits September 1, 2025 08:20

move up lines

6bc36b5

Update Mathlib/Algebra/QuadraticAlgebra.lean

d764fa3

Co-authored-by: Eric Wieser <[email protected]>

Tidy variables

4a98610

Add IsCentralScalar instance for QuadraticAlgebra

af979f7

Whysoserioushah requested a review from alreadydone September 1, 2025 00:31

eric-wieser changed the title ~~feat(Algebra/QuadraticAlgebra) : Define Quadratic Algebra~~ feat(Algebra/QuadraticAlgebra): Define Quadratic Algebra Sep 2, 2025

eric-wieser reviewed Sep 3, 2025

View reviewed changes

Comment thread Mathlib/Algebra/QuadraticAlgebra.lean

whitespace

6c4a7c4

riccardobrasca approved these changes Sep 3, 2025

View reviewed changes

Update Mathlib/Algebra/QuadraticAlgebra.lean

1f2da52

Co-authored-by: Eric Wieser <[email protected]>

YaelDillies changed the title ~~feat(Algebra/QuadraticAlgebra): Define Quadratic Algebra~~ feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras Sep 5, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Sep 5, 2025

mathlib-bors bot changed the title ~~feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras~~ [Merged by Bors] - feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras Sep 5, 2025

mathlib-bors bot closed this Sep 5, 2025

Conversation

Nebula691 commented Jul 26, 2025 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4a2cfa2512

Import changes for modified files

Declarations diff

Uh oh!

kckennylau left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kckennylau Jul 26, 2025

Choose a reason for hiding this comment

Uh oh!

Whysoserioushah Jul 26, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

YaelDillies commented Sep 2, 2025

Uh oh!

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Sep 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

riccardobrasca commented Sep 5, 2025

Uh oh!

mathlib-bors bot commented Sep 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

11 participants

Nebula691 commented Jul 26, 2025 •

edited by eric-wieser

Loading

github-actions bot commented Jul 26, 2025 •

edited

Loading