Commit 2025-06-27 14:36 3f90fd59

View on Github →

fix: generalize CommSemiring to Semiring for bilinear map composition (#26458) This file could do with further variable cleanup, but that's left for a later PR. I needed some of these generalizations for some base change results.

Estimated changes

modified def LinearMap.compl₁₂
modified theorem LinearMap.compl₁₂_apply
modified theorem LinearMap.compl₁₂_id_id
modified theorem LinearMap.compl₁₂_inj
modified def LinearMap.compl₂
modified theorem LinearMap.compl₂_apply
modified theorem LinearMap.compl₂_id
modified def LinearMap.lcomp
modified def LinearMap.lcompₛₗ