Commit 2025-04-28 09:04 d60509c1

View on Github →

chore: move Module.End-related decls to the Module.End namespace (#23705) No deprecations, since they would clash across namespaces. From Toric

Estimated changes

modified theorem fwdDiff_aux.shiftₗ_apply
added theorem Module.End.isUnit_iff
deleted theorem Module.End_isUnit_iff
deleted theorem LinearMap.coe_mul
deleted theorem LinearMap.coe_one
deleted theorem LinearMap.coe_pow
deleted theorem LinearMap.id_pow
deleted theorem LinearMap.iterate_succ
deleted theorem LinearMap.mul_apply
deleted theorem LinearMap.mul_eq_comp
deleted theorem LinearMap.one_apply
deleted theorem LinearMap.one_eq_id
deleted theorem LinearMap.pow_apply
added theorem Module.End.coe_mul
added theorem Module.End.coe_one
added theorem Module.End.coe_pow
added theorem Module.End.id_pow
modified theorem Module.End.intCast_apply
added theorem Module.End.mul_apply
added theorem Module.End.mul_eq_comp
modified theorem Module.End.natCast_apply
modified theorem Module.End.ofNat_apply
added theorem Module.End.one_apply
added theorem Module.End.one_eq_id
added theorem Module.End.pow_apply
deleted theorem LinearMap.pow_restrict
modified theorem LinearMap.trace_id