proposition: Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H) (n : nat) (g : G) : f (grp_pow g n) = grp_pow (f g) n.
proof: Proof. induction n. + cbn. apply grp_homo_unit. + cbn. refine ((grp_homo_op f g (grp_pow g n)) @ _). exact (ap (fun m => f g + m) IHn). Defined.
imports: Basics Types HProp HFiber HSet PathAny (notations) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.canonical_names Classes.interfaces.canonical_names (SgOp, sg_op, One, one, MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity) Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, negate_l, negate_r, IsSemiGroup(..), sg_set, sg_ass, IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup, IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor, IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit) Classes.theory.groups Pointed.Core WildCat Spaces.Nat.Core Truncations.Core