Theorem LinearEquiv.smul_apply

Modification history

2026-10-29 16:29
Mathlib/Algebra/Module/Equiv/Defs.lean
feat: use `IsApply` for `LinearEquiv` (#45391) …
Deleted LinearEquiv.smul_applyView on Github →
2026-02-10 19:29
Mathlib/Algebra/Module/Equiv/Defs.lean
feat: `{Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv` are "almost" injective (#33417) …
Added LinearEquiv.smul_applyView on Github →