rangeRestrict — Mathlib

English

The canonical surjective group homomorphism rangeRestrict: G →* f.range is surjective.

Русский

Канонический сюръективный гомоморфизм rangeRestrict: G →* f.range является сюръективным.

LaTeX

$$Surjective(rangeRestrict(f))$$

Lean4

/-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
homomorphism `G →* N`. -/
@[to_additive /-- The canonical surjective `AddGroup` homomorphism `G →+ f(G)` induced by a group
          homomorphism `G →+ N`. -/
    ]
def rangeRestrict (f : G →* N) : G →* f.range :=
  codRestrict f _ fun x => ⟨x, rfl⟩

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