case intro
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
A : Type u_1
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
n : ℕ
Ei : Fin (Nat.succ (Nat.succ n)) → Type wEi
inst✝¹ : (i : Fin (Nat.succ (Nat.succ n))) → NormedAddCommGroup (Ei i)
inst✝ : (i : Fin (Nat.succ (Nat.succ n))) → NormedSpace 𝕜 (Ei i)
hn : 0 < Nat.succ n
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ n) A‖ ≤ 1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
hn : 0 < n
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
no goals
case intro
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
A : Type u_1
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
n : ℕ
Ei : Fin (Nat.succ (Nat.succ n)) → Type wEi
inst✝¹ : (i : Fin (Nat.succ (Nat.succ n))) → NormedAddCommGroup (Ei i)
inst✝ : (i : Fin (Nat.succ (Nat.succ n))) → NormedSpace 𝕜 (Ei i)
hn : 0 < Nat.succ n
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ n) A‖ ≤ 1
exact norm_mkPiAlgebraFin_succ_le