Theorem LinearEquiv.coe_addEquiv_apply

Modification history

2025-07-01 00:55
Mathlib/Algebra/Module/Equiv/Defs.lean
chore: bump toolchain to v4.22.0-rc2 (#26564) …
Modified LinearEquiv.coe_addEquiv_applyView on Github →
2025-02-05 15:13
Mathlib/Algebra/Module/Equiv/Defs.lean
chore(LinearAlgebra/TensorProduct): upgrade `TensorProduct.prodRight` (#21432) …
Added LinearEquiv.coe_addEquiv_applyView on Github →