of_injective_mulHom — Mathlib

English

If H embeds into G via an injective MulHom and G has TwoUniqueProds, then H has TwoUniqueProds.

Русский

Если H инъектно в G через MulHom и G имеет TwoUniqueProds, то H имеет TwoUniqueProds.

LaTeX

$$$ \\forall G,H\\, (f: H \\to_* G), \\text{Injective}(f) \\Rightarrow \\mathrm{TwoUniqueProds} G \\Rightarrow \\mathrm{TwoUniqueProds} H.$$$

Lean4

@[to_additive]
theorem of_injective_mulHom (f : H →ₙ* G) (hf : Function.Injective f) (_ : TwoUniqueProds G) : TwoUniqueProds H :=
  of_mulHom f (fun _ _ _ _ _ ↦ .imp (hf ·) (hf ·))

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