Commit 2024-12-20 14:36 42764fbc

View on Github →

chore: generalise ‖a ^ n‖ ≤ n * ‖a‖ to non-abelian groups (#20110) From LeanCamCombi

Estimated changes

modified theorem nnnorm_pow_le_mul_norm
modified theorem norm_pow_le_mul_norm