English
If B i = 1, then for all k ∈ K and y ∈ L, B.norm((algebraMap K L) k · y) = B.norm(algebraMap K L k) · B.norm y.
Русский
Если B_i = 1, то для всех k ∈ K и y ∈ L выполняется B.norm((algebraMap K L) k · y) = B.norm(algebraMap K L k) · B.norm y.
LaTeX
$$$\forall k\in K,\; \forall y\in L,\ B.norm((\mathrm{algebraMap} \\ K \\ L)\ k \cdot y) = B.norm((\mathrm{algebraMap} \\ K \\ L)\ k) \cdot B.norm y$$$
Lean4
/-- For any `k : K`, `y : L`, we have
`B.norm ((algebra_map K L) k * y) = B.norm ((algebra_map K L) k) * B.norm y`. -/
theorem norm_smul {ι : Type*} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι} (hBi : B i = (1 : L)) (k : K) (y : L) :
B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y :=
by
by_cases hk : k = 0
· rw [hk, map_zero, zero_mul, B.norm_zero, zero_mul]
· rw [norm_extends hBi]
obtain ⟨i, _, hi⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖B.repr y i‖)
obtain ⟨j, _, hj⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖)
have hij : ‖B.repr y i‖ = ‖B.repr y j‖ := by
rw [← hi]
apply le_antisymm _ (norm_repr_le_norm B j)
have hj' := Finset.le_sup' (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖) (mem_univ i)
simp only [repr_smul', norm_mul, ← hi] at hj hj'
exact (mul_le_mul_iff_right₀ (lt_of_le_of_ne (norm_nonneg _) (Ne.symm (norm_ne_zero_iff.mpr hk)))).mp (hj ▸ hj')
simp only [norm, hj]
rw [repr_smul', norm_mul, hi, hij]
