case zero
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.980529
inst✝¹⁷ : Monoid R'
R'' : Type ?u.980535
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.980547
Q : Type ?u.980550
S : Type ?u.980553
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.981680
Q' : Type ?u.981683
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ map f g ^ Nat.zero = map (f ^ Nat.zero) (g ^ Nat.zero)

case succ
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.980529
inst✝¹⁷ : Monoid R'
R'' : Type ?u.980535
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.980547
Q : Type ?u.980550
S : Type ?u.980553
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.981680
Q' : Type ?u.981683
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
ih : map f g ^ n = map (f ^ n) (g ^ n)
⊢ map f g ^ Nat.succ n = map (f ^ Nat.succ n) (g ^ Nat.succ n)
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.980529
inst✝¹⁷ : Monoid R'
R'' : Type ?u.980535
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.980547
Q : Type ?u.980550
S : Type ?u.980553
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.981680
Q' : Type ?u.981683
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
⊢ map f g ^ n = map (f ^ n) (g ^ n)
induction' n with n ih
no goals
case zero
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.980529
inst✝¹⁷ : Monoid R'
R'' : Type ?u.980535
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.980547
Q : Type ?u.980550
S : Type ?u.980553
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.981680
Q' : Type ?u.981683
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ map f g ^ Nat.zero = map (f ^ Nat.zero) (g ^ Nat.zero)
simp only [Nat.zero_eq, pow_zero, map_one]
no goals
case succ
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.980529
inst✝¹⁷ : Monoid R'
R'' : Type ?u.980535
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.980547
Q : Type ?u.980550
S : Type ?u.980553
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.981680
Q' : Type ?u.981683
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
ih : map f g ^ n = map (f ^ n) (g ^ n)
⊢ map f g ^ Nat.succ n = map (f ^ Nat.succ n) (g ^ Nat.succ n)
simp only [pow_succ', ih, map_mul]