case zero
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
⊢ ↑(f ^ Nat.zero) m = (↑f^[Nat.zero]) m

case succ
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
n : ℕ
ih : ↑(f ^ n) m = (↑f^[n]) m
⊢ ↑(f ^ Nat.succ n) m = (↑f^[Nat.succ n]) m
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
n : ℕ
m : M
⊢ ↑(f ^ n) m = (↑f^[n]) m
induction' n with n ih
no goals
case zero
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
⊢ ↑(f ^ Nat.zero) m = (↑f^[Nat.zero]) m
rfl
case succ
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
n : ℕ
ih : ↑(f ^ n) m = (↑f^[n]) m
⊢ ↑f ((↑f^[n]) m) = (↑f^[n]) (↑f m)
case succ
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
n : ℕ
ih : ↑(f ^ n) m = (↑f^[n]) m
⊢ ↑(f ^ Nat.succ n) m = (↑f^[Nat.succ n]) m
simp only [Function.comp_apply, Function.iterate_succ, LinearMap.mul_apply, pow_succ, ih]
no goals
case succ
R : Type u_1
R₁ : Type ?u.141510
R₂ : Type ?u.141513
R₃ : Type ?u.141516
R₄ : Type ?u.141519
S : Type ?u.141522
K : Type ?u.141525
K₂ : Type ?u.141528
M : Type u_2
M' : Type ?u.141534
M₁ : Type ?u.141537
M₂ : Type ?u.141540
M₃ : Type ?u.141543
M₄ : Type ?u.141546
N : Type ?u.141549
N₂ : Type ?u.141552
ι : Type ?u.141555
V : Type ?u.141558
V₂ : Type ?u.141561
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₗ[R] M
m : M
n : ℕ
ih : ↑(f ^ n) m = (↑f^[n]) m
⊢ ↑f ((↑f^[n]) m) = (↑f^[n]) (↑f m)
exact (Function.Commute.iterate_self _ _ m).symm