Theorem: toCircle_smul (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
x : AddCircle T
⊢ (n • x).toCircle = x.toCircle ^ n
Tactic:
induction' x using QuotientAddGroup.induction_on' with z
State after:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ (n • ↑z).toCircle = AddCircle.toCircle ↑z ^ n

State before:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ (n • ↑z).toCircle = AddCircle.toCircle ↑z ^ n
Tactic:
rw [←AddCircle.coe_nsmul]
State after:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ AddCircle.toCircle ↑(n • z) = AddCircle.toCircle ↑z ^ n

State before:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ AddCircle.toCircle ↑(n • z) = AddCircle.toCircle ↑z ^ n
Tactic:
simp only [AddCircle.toCircle, Function.Periodic.lift_coe]
State after:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n

State before:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
n : ℕ
z : ℝ
⊢ expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
Tactic:
induction' n with n h
State after:
case H.zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z : ℝ
⊢ expMapCircle (2 * π / T * 0 • z) = expMapCircle (2 * π / T * z) ^ 0

case H.succ
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z : ℝ
n : ℕ
h : expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
⊢ expMapCircle (2 * π / T * (n + 1) • z) = expMapCircle (2 * π / T * z) ^ (n + 1)

State before:
case H.zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z : ℝ
⊢ expMapCircle (2 * π / T * 0 • z) = expMapCircle (2 * π / T * z) ^ 0
Tactic:
simp only [expMapCircle_zero, nsmul_eq_mul, algebraMap.coe_zero, MulZeroClass.zero_mul,
  MulZeroClass.mul_zero, pow_zero, Nat.zero_eq, zero_smul, Function.Periodic.lift_coe]
State after:
no goals

State before:
case H.succ
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z : ℝ
n : ℕ
h : expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
⊢ expMapCircle (2 * π / T * (n + 1) • z) = expMapCircle (2 * π / T * z) ^ (n + 1)
Tactic:
simp only [succ_nsmul, left_distrib, expMapCircle_add, h, pow_succ]
State after:
no goals