Theorem linearIndependent_algHom_toLinearMap'

Modification history

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 →