Theorem LinearEquiv.mul_apply

Modification history

2026-10-29 16:29
Mathlib/Algebra/Module/Equiv/Basic.lean
feat: use `IsApply` for `LinearEquiv` (#45391) …
Deleted LinearEquiv.mul_applyView on Github →
2024-12-06 05:31
Mathlib/Algebra/Module/Equiv/Basic.lean
feat: power of product of two reflections (#13270) …
Added LinearEquiv.mul_applyView on Github →