Commit 2025-11-01 12:56 4a98d4f5

View on Github →

feat(Mathlib/Algebra/QuadraticAlgebra): norm, star structure on quadratic alg. (#30059) Define the norm and the star structure on a quadratic algebra. Application to the units, the zero divisors and the field structure (when there is one).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Basic.lean

added theorem mul_mul_mul_comm'

Modified Mathlib/Algebra/QuadraticAlgebra.lean

added theorem QuadraticAlgebra.coe_dvd_iff

added theorem QuadraticAlgebra.coe_dvd_iff_dvd

added theorem QuadraticAlgebra.coe_eq_one_iff

added theorem QuadraticAlgebra.coe_eq_zero_iff

added theorem QuadraticAlgebra.nsmul_mk

added theorem QuadraticAlgebra.zsmul_val

Created Mathlib/Algebra/QuadraticAlgebra/Basic.lean

added theorem QuadraticAlgebra.algHom_ext

added theorem QuadraticAlgebra.coe_mem_nonZeroDivisors_iff

added theorem QuadraticAlgebra.coe_norm_eq_mul_star

added theorem QuadraticAlgebra.im_star

added theorem QuadraticAlgebra.isUnit_iff_norm_isUnit

added def QuadraticAlgebra.lift

added theorem QuadraticAlgebra.mk_eq_add_smul_omega

added theorem QuadraticAlgebra.mker_norm_eq_unitary

added theorem QuadraticAlgebra.mul_star

added def QuadraticAlgebra.norm

added theorem QuadraticAlgebra.norm_coe

added theorem QuadraticAlgebra.norm_def

added theorem QuadraticAlgebra.norm_eq_one_iff_mem_unitary

added theorem QuadraticAlgebra.norm_eq_zero_iff_eq_zero

added theorem QuadraticAlgebra.norm_intCast

added theorem QuadraticAlgebra.norm_mem_nonZeroDivisors_iff

added theorem QuadraticAlgebra.norm_natCast

added theorem QuadraticAlgebra.norm_neg

added theorem QuadraticAlgebra.norm_one

added theorem QuadraticAlgebra.norm_star

added theorem QuadraticAlgebra.norm_zero

added def QuadraticAlgebra.omega

added theorem QuadraticAlgebra.omega_im

added theorem QuadraticAlgebra.omega_mul_coe_mul_mk

added theorem QuadraticAlgebra.omega_mul_mk

added theorem QuadraticAlgebra.omega_mul_omega_eq_add

added theorem QuadraticAlgebra.omega_mul_omega_eq_mk

added theorem QuadraticAlgebra.omega_re

added theorem QuadraticAlgebra.re_star

added theorem QuadraticAlgebra.star_mem_nonZeroDivisors

added theorem QuadraticAlgebra.star_mem_nonZeroDivisors_iff

added theorem QuadraticAlgebra.star_mk