ker_leftRegular_norm_eq — Mathlib

English

The kernel of the left-regular norm map equals the kernel of the linearCombination map: ker((leftRegular k G).norm) = ker(linearCombination k (fun _ => (1 : k))).

Русский

Ядро отображения нормы левого регулярного действия равно ядру отображения линейной комбинации по единицам: ker((leftRegular k G).norm) = ker(linearCombination k (fun _ => 1)).

LaTeX

$$$ \\ker\\bigl( (leftRegular k G).norm \\bigr) = \\ker\\bigl( linearCombination k (\\text{fun } _ => 1) \\bigr) $$$

Lean4

theorem ker_leftRegular_norm_eq :
    LinearMap.ker (leftRegular k G).norm = LinearMap.ker (linearCombination k (fun _ => (1 : k))) :=
  by
  ext
  exact leftRegular_norm_eq_zero_iff _

Похожие утверждения