Commit 2023-11-24 18:46 bae5525c

View on Github →

style(Algebra): write coe_pow lemmas more clearly (#8292)

Estimated changes

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

modified theorem WithZero.coe_zpow

Modified Mathlib/Data/Rat/Cast/CharZero.lean

modified theorem Rat.cast_pow

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

modified theorem SubMulAction.coe_pow

modified theorem SubMulAction.subset_coe_pow