Commit 2026-02-10 22:14 06659560

View on Github →

refactor: add type synonym for convolutive product of linear maps and intrinsic star (#34945) ... to avoid instance conflicts. Currently, the instances in the scopes IntrinsicStar and ConvolutionProduct (LinearMap.intrinsicStar and LinearMap.convMul) conflict with global instances. This fixes that. This also allows us to have these instances globally rather than scoped with a possible conflict. We follow the same implementation as with WithLp. We provide the type synonym as a structure to ensure that there will be no defeq abuse. The WithConv type synonym is defined for any type A so that we can have WithConv (LinearMap R E F), WithConv (ContinuousLinearMap R E F) and WithConv (Matrix m n R).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Star/LinearMap.lean

modified theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star

modified theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'

deleted def LinearMap.intrinsicInvolutiveStar

deleted def LinearMap.intrinsicStar

deleted def LinearMap.intrinsicStarAddMonoid

deleted theorem LinearMap.intrinsicStarModule

modified theorem LinearMap.intrinsicStar_apply

modified theorem LinearMap.intrinsicStar_comp

modified theorem LinearMap.intrinsicStar_eq_comp

modified theorem LinearMap.intrinsicStar_id

modified theorem LinearMap.intrinsicStar_lTensor

modified theorem LinearMap.intrinsicStar_mulLeft

modified theorem LinearMap.intrinsicStar_mulRight

modified theorem LinearMap.intrinsicStar_rTensor

modified theorem LinearMap.intrinsicStar_smulRight

modified theorem LinearMap.intrinsicStar_zero

modified theorem LinearMap.toMatrix'_intrinsicStar

modified theorem Matrix.intrinsicStar_toLin'

modified theorem Module.End.IsUnit.intrinsicStar

deleted def Module.End.Units.intrinsicStar

modified theorem Module.End.isUnit_intrinsicStar_iff

modified theorem Module.End.mem_eigenspace_intrinsicStar_iff

modified theorem Module.End.spectrum_intrinsicStar

modified theorem TensorProduct.intrinsicStar_map

Created Mathlib/Algebra/WithConv.lean

added theorem WithConv.equiv_apply

added theorem WithConv.linearEquiv_apply

added theorem WithConv.ofConv_add

added theorem WithConv.ofConv_bijective

added theorem WithConv.ofConv_eq_zero

added theorem WithConv.ofConv_injective

added theorem WithConv.ofConv_listSum

added theorem WithConv.ofConv_multisetSum

added theorem WithConv.ofConv_neg

added theorem WithConv.ofConv_smul

added theorem WithConv.ofConv_sub

added theorem WithConv.ofConv_sum

added theorem WithConv.ofConv_surjective

added theorem WithConv.ofConv_toConv

added theorem WithConv.ofConv_zero

added theorem WithConv.symm_equiv_apply

added theorem WithConv.symm_linearEquiv_apply

added theorem WithConv.toAddEquiv_linearEquiv

added theorem WithConv.toConv_add

added theorem WithConv.toConv_bijective

added theorem WithConv.toConv_eq_zero

added theorem WithConv.toConv_injective

added theorem WithConv.toConv_listSum

added theorem WithConv.toConv_multisetSum

added theorem WithConv.toConv_neg

added theorem WithConv.toConv_ofConv

added theorem WithConv.toConv_smul

added theorem WithConv.toConv_sub

added theorem WithConv.toConv_sum

added theorem WithConv.toConv_surjective

added theorem WithConv.toConv_zero

added theorem WithConv.toEquiv_addEquiv

added structure WithConv

Modified Mathlib/RingTheory/Coalgebra/Convolution.lean

modified theorem Coalgebra.Repr.convMul_apply

modified theorem LinearMap.algHom_comp_convMul_distrib

modified theorem LinearMap.convMul_apply

modified theorem LinearMap.convMul_def

modified theorem LinearMap.convOne_apply

modified theorem LinearMap.convOne_def