lift_ext — Mathlib

English

The natural map of generators into the free abelian group is injective.

Русский

Естественная карта генераторов в свободную абелеву группу инъективна.

LaTeX

$$$\\forall x:\\; FreeAbelianGroup.of(x) \\neq 0$ implies injectivity of of$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem lift_ext (g h : FreeAbelianGroup α →+ β) (H : ∀ x, g (of x) = h (of x)) : g = h :=
  lift.symm.injective <| funext H

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