map_isConj — Mathlib

English

A monoid homomorphism preserves conjugacy: If IsConj a b, then IsConj (f a) (f b).

Русский

Гомоморфизация моноид сохраняет конъугированность: IsConj a b ⇒ IsConj (f a) (f b).

LaTeX

$$$\\\\forall f : \\alpha \\to \\beta, \\\\forall a b, IsConj(a,b) \\Rightarrow IsConj(f(a), f(b))$$$

Lean4

protected theorem map_isConj (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)
  | ⟨c, hc⟩ => ⟨Units.map f c, by rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]⟩

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