coe_mul — Mathlib

English

The inclusion map from a subgroup H to G preserves multiplication: for all x,y in H, the image of their product equals the product of their images.

Русский

Включение подгруппы H в группу G сохраняет умножение: для всех x,y ∈ H образ произведения равен произведению образов.

LaTeX

$$$\forall x,y \in H, \uparrow(x y) = \uparrow x \cdot \uparrow y$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y :=
  rfl

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