Commit 2023-09-18 15:32 a2e8c03e

View on Github →

chore: move some lemmas about LinearMap pow/comp earlier (#7158)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem LinearMap.coe_pow

added theorem LinearMap.commute_pow_left_of_commute

added theorem LinearMap.comp_assoc

added theorem LinearMap.id_pow

added theorem LinearMap.injective_of_iterate_injective

added theorem LinearMap.iterate_bijective

added theorem LinearMap.iterate_injective

added theorem LinearMap.iterate_succ

added theorem LinearMap.iterate_surjective

added theorem LinearMap.pow_apply

added theorem LinearMap.pow_map_zero_of_le

added theorem LinearMap.surjective_of_iterate_surjective

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearMap.coe_pow

deleted theorem LinearMap.commute_pow_left_of_commute

deleted theorem LinearMap.comp_assoc

deleted theorem LinearMap.id_pow

deleted theorem LinearMap.injective_of_iterate_injective

deleted theorem LinearMap.iterate_bijective

deleted theorem LinearMap.iterate_injective

deleted theorem LinearMap.iterate_succ

deleted theorem LinearMap.iterate_surjective

deleted theorem LinearMap.pow_apply

deleted theorem LinearMap.pow_map_zero_of_le

deleted theorem LinearMap.surjective_of_iterate_surjective