quotientKerEquivOfSurjective — Mathlib

English

If A' = B' and A = B, then the quotients A/(A' ∩ A) and B/(B' ∩ B) are isomorphic.

Русский

Если A' = B' и A = B, то факторы A/(A' ∩ A) и B/(B' ∩ B) изоморфны.

LaTeX

$$A' = B' and A = B imply A/(A' ∩ A) ≃* B/(B' ∩ B)$$

Lean4

/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.

For a `computable` version, see `QuotientGroup.quotientKerEquivOfRightInverse`.
-/
@[to_additive /-- The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
    For a `computable` version, see `QuotientAddGroup.quotientKerEquivOfRightInverse`. -/
    ]
noncomputable def quotientKerEquivOfSurjective (hφ : Surjective φ) : G ⧸ ker φ ≃* H :=
  quotientKerEquivOfRightInverse φ _ hφ.hasRightInverse.choose_spec

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