of_injective_mulHom — Mathlib

English

If H maps injectively into G via a multiplicative homomorphism f and G has UniqueProds, then H also has UniqueProds.

Русский

Если через инъективный мультигомоморфизм f множество H отображается в G, и G обладает UniqueProds, то и H обладает UniqueProds.

LaTeX

$$$ \\forall G,H\\,[\\text{Mul }G][\\text{Mul }H] (f: H \\to_* G), \\mathrm{Injective} (f) \\Rightarrow \\mathrm{UniqueProds }G \\Rightarrow \\mathrm{UniqueProds }H.$$$

Lean4

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

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