Commit 2025-09-05 19:23 62eeacf8

View on Github →

feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras (#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)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/QuadraticAlgebra.lean

added theorem QuadraticAlgebra.algebraMap_eq

added theorem QuadraticAlgebra.algebraMap_injective

added theorem QuadraticAlgebra.basis_repr_apply

added def QuadraticAlgebra.coe

added theorem QuadraticAlgebra.coe_add

added theorem QuadraticAlgebra.coe_algebraMap

added theorem QuadraticAlgebra.coe_inj

added theorem QuadraticAlgebra.coe_injective

added theorem QuadraticAlgebra.coe_intCast

added theorem QuadraticAlgebra.coe_mul

added theorem QuadraticAlgebra.coe_mul_eq_smul

added theorem QuadraticAlgebra.coe_natCast

added theorem QuadraticAlgebra.coe_neg

added theorem QuadraticAlgebra.coe_ofNat

added theorem QuadraticAlgebra.coe_one

added theorem QuadraticAlgebra.coe_pow

added theorem QuadraticAlgebra.coe_smul

added theorem QuadraticAlgebra.coe_sub

added theorem QuadraticAlgebra.coe_zero

added def QuadraticAlgebra.equivProd

added theorem QuadraticAlgebra.finrank_eq_two

added theorem QuadraticAlgebra.im_add

added theorem QuadraticAlgebra.im_coe

added theorem QuadraticAlgebra.im_intCast

added theorem QuadraticAlgebra.im_mul

added theorem QuadraticAlgebra.im_natCast

added theorem QuadraticAlgebra.im_neg

added theorem QuadraticAlgebra.im_ofNat

added theorem QuadraticAlgebra.im_one

added theorem QuadraticAlgebra.im_smul

added theorem QuadraticAlgebra.im_sub

added theorem QuadraticAlgebra.im_zero

added def QuadraticAlgebra.imₗ

added def QuadraticAlgebra.linearEquivTuple

added theorem QuadraticAlgebra.linearEquivTuple_apply

added theorem QuadraticAlgebra.linearEquivTuple_symm_apply

added theorem QuadraticAlgebra.mk_add_mk

added theorem QuadraticAlgebra.mk_eta

added theorem QuadraticAlgebra.mk_mul_mk

added theorem QuadraticAlgebra.mk_sub_mk

added theorem QuadraticAlgebra.mul_coe_eq_smul

added theorem QuadraticAlgebra.neg_mk

added theorem QuadraticAlgebra.rank_eq_two

added theorem QuadraticAlgebra.re_add

added theorem QuadraticAlgebra.re_coe

added theorem QuadraticAlgebra.re_intCast

added theorem QuadraticAlgebra.re_mul

added theorem QuadraticAlgebra.re_natCast

added theorem QuadraticAlgebra.re_neg

added theorem QuadraticAlgebra.re_ofNat

added theorem QuadraticAlgebra.re_one

added theorem QuadraticAlgebra.re_smul

added theorem QuadraticAlgebra.re_sub

added theorem QuadraticAlgebra.re_zero

added def QuadraticAlgebra.reₗ

added theorem QuadraticAlgebra.smul_coe

added theorem QuadraticAlgebra.smul_mk

added structure QuadraticAlgebra