rangeKerLift — Mathlib

English

The map rangeKerLift φ: G/ker φ → φ.range is injective.

Русский

Карта rangeKerLift φ: G/ker φ → range φ инъективна.

LaTeX

$$Injective (rangeKerLift φ)$$

Lean4

/-- The induced map from the quotient by the kernel to the range. -/
@[to_additive /-- The induced map from the quotient by the kernel to the range. -/
    ]
def rangeKerLift : G ⧸ ker φ →* φ.range :=
  lift _ φ.rangeRestrict fun g hg => mem_ker.mp <| by rwa [ker_rangeRestrict]

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