noncommCoprod_unique — Mathlib

English

If each m commutes with the image of ϕ_i, then m commutes with the whole noncommPiCoprod ϕ.

Русский

Если для каждого i и элемента m выполняется, что m коммутирует с образами ϕ_i, тогда m коммутирует с целым noncommPiCoprod ϕ.

LaTeX

$$$\\forall m\\in M,\\; (\\forall i, x\\in N_i, \\ \\mathrm{Commute}(m, ϕ_i(x))) \\Rightarrow \\mathrm{Commute}(m, (\\mathrm{noncommPiCoprod } ϕ hcomm))$$$

Lean4

@[to_additive (attr := simp)]
theorem noncommCoprod_unique (f : M × N →* P) :
    (f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) (fun _ _ => (commute_inl_inr _ _).map f) = f :=
  ext fun x => by simp [inl_apply, inr_apply, ← map_mul]

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