Commit 2023-07-24 16:15 739d98d5

View on Github →

feat: add 2 coe_pow lemmas (#6063) Also drop @[simp] on LinearMap.pow_apply.

Estimated changes

Modified Mathlib/Algebra/Lie/Weights.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Modified Mathlib/Analysis/NormedSpace/LinearIsometry.lean

added theorem LinearIsometry.coe_pow

Modified Mathlib/LinearAlgebra/Basic.lean

modified theorem LinearMap.coe_pow

modified theorem LinearMap.pow_apply

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem ContinuousLinearMap.coe_pow