comap_id — Mathlib

English

Composing with the identity multiplicative homomorphism leaves a subsemigroup unchanged.

Русский

Композиция с тождественным мультипликативным гомомоморфизмом оставляет подполугруппу неизменной.

LaTeX

$$$\\forall S : \\text{Subsemigroup } P,\\; S.comap (\\text{MulHom.id } P) = S$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_id (S : Subsemigroup P) : S.comap (MulHom.id _) = S :=
  ext (by simp)

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