Theorem linearIndependent_algHom_toLinearMap'

Modification history

2026-01-13 19:40

Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified linearIndependent_algHom_toLinearMap'View on Github →

2025-02-25 23:58

Mathlib/LinearAlgebra/LinearIndependent.lean

chore(LinearAlgebra): split LinearIndependent into Defs, Basic, Lemmas (#22065) …

Modified linearIndependent_algHom_toLinearMap'View on Github →

2024-01-12 18:56

Mathlib/LinearAlgebra/LinearIndependent.lean

feat(LinearAlgebra): generalize results about `Module.rank` of `LinearMap`. (#9677) …

Modified linearIndependent_algHom_toLinearMap'View on Github →

2024-01-06 13:21

Mathlib/LinearAlgebra/LinearIndependent.lean

feat: Cyclic extensions are kummer. (#9368)

Added linearIndependent_algHom_toLinearMap'View on Github →