Theorem LinearIndependent.linearCombinationEquiv_apply_coe

Modification history

2025-08-21 13:56
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
chore(*): address some `@[simps]` porting notes (#28517) …
Deleted LinearIndependent.linearCombinationEquiv_apply_coeView on Github →
2025-02-25 23:58
Mathlib/LinearAlgebra/LinearIndependent.lean
chore(LinearAlgebra): split LinearIndependent into Defs, Basic, Lemmas (#22065) …
Modified LinearIndependent.linearCombinationEquiv_apply_coeView on Github →
2024-08-30 00:21
Mathlib/LinearAlgebra/LinearIndependent.lean
chore: rename Finsupp.total (#16277) …
Added LinearIndependent.linearCombinationEquiv_apply_coeView on Github →