Theorem WithConv.symm_linearEquiv_apply

Modification history

2026-02-10 22:14
Mathlib/Algebra/WithConv.lean
refactor: add type synonym for convolutive product of linear maps and intrinsic star (#34945) …
Added WithConv.symm_linearEquiv_applyView on Github →