map_isMulCommutative — Mathlib

English

If H is Mul-Commutative, then H.map f is Mul-Commutative.

Русский

Если H — мультипликативно коммутативная подгруппа, то образ H под отображением f также мультипликативно коммутативен.

LaTeX

$$$ [\\mathrm{IsMulCommutative}\\ H] \\Rightarrow \\mathrm{IsMulCommutative}(H.map\ f) $$$

Lean4

@[to_additive]
instance map_isMulCommutative (f : G →* G') [IsMulCommutative H] : IsMulCommutative (H.map f) :=
  ⟨⟨by
      rintro ⟨-, a, ha, rfl⟩ ⟨-, b, hb, rfl⟩
      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← map_mul, ← map_mul]
      exact congr_arg f (Subtype.ext_iff.mp (mul_comm (⟨a, ha⟩ : H) ⟨b, hb⟩))⟩⟩

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