kerLift_injective — Mathlib

English

The kernel lift map kerLift φ is injective: equality of images implies equality of cosets.

Русский

Карта kerLift φ инъективна: равенство образов в H означает равенство соответствующих косет.

LaTeX

$$Injective (kerLift φ)$$

Lean4

@[to_additive]
theorem kerLift_injective : Injective (kerLift φ) := fun a b =>
  Quotient.inductionOn₂' a b fun a b (h : φ a = φ b) =>
    Quotient.sound' <| by
      rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
        -- Note that `ker φ` isn't definitionally `ker (φ.rangeRestrict)`
        -- so there is a bit of annoying code duplication here

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