comap_injective_isMulCommutative — Mathlib

English

If f is injective and H is Mul-Commutative, then H.comap f is Mul-Commutative.

Русский

Если f инъективно, и H мультикоммутативна, то H.comap f тоже мультикоммутативна.

LaTeX

$$$ \\text{Injective}(f) \\Rightarrow [\\mathrm{IsMulCommutative} (H.comap f)] $$$

Lean4

@[to_additive]
theorem comap_injective_isMulCommutative {f : G' →* G} (hf : Injective f) [IsMulCommutative H] :
    IsMulCommutative (H.comap f) :=
  ⟨⟨fun a b =>
      Subtype.ext
        (by
          have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
          rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul, hf.eq_iff] at this)⟩⟩

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