Commit 2024-01-08 21:36 a6cf8f57

View on Github →

feat(Algebra/GroupPower): Miscellaneous lemmas (#9388) Generalise pow_ite/ite_pow and give a version of pow_add_pow_le that doesn't require the exponent to be nonzero. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem dite_pow

added theorem ite_pow

added theorem pow_dite

added theorem pow_ite

Modified Mathlib/Algebra/GroupPower/Basic.lean

deleted theorem ite_pow

deleted theorem pow_ite

Modified Mathlib/Algebra/GroupPower/Order.lean

added theorem pow_add_pow_le'

Modified Mathlib/Algebra/SMulWithZero.lean

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

deleted theorem ite_smul

deleted theorem smul_ite