map_one_eq_bot — Mathlib

English

For any subgroup K of G, the image of K under the zero (trivial) homomorphism to N is the bottom subgroup of N.

Русский

Для подгруппы K подгруппы G образ подгруппы K нулевым гомоморфизмом в N — это нижняя подгруппа, т.е. ⊥.

LaTeX

$$$\\mathrm{map}_{1}(K) = \\bot.$$$

Lean4

@[to_additive (attr := simp)]
theorem map_one_eq_bot : K.map (1 : G →* N) = ⊥ :=
  eq_bot_iff.mpr <| by
    rintro x ⟨y, _, rfl⟩
    simp

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