norm_surjective — Mathlib

English

For any nonempty α, the norm map from FreeGroup α is surjective.

Русский

Для любого непустого множества α отображение нормы из FreeGroup α является сюръективным.

LaTeX

$$$$\\forall {\\\\alpha} [\\\\text{Nonempty }\\\\alpha],\\\\; \\operatorname{Surjective}(\\\\mathrm{norm}_{\\\\alpha}).$$$$

Lean4

@[to_additive]
theorem norm_surjective [Nonempty α] : Function.Surjective (norm (α := α)) :=
  by
  let ⟨a⟩ := ‹Nonempty α›
  exact Function.RightInverse.surjective <| norm_of_pow a

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