coe_div — Mathlib

English

The division in a subgroup corresponds to division in the ambient group via the inclusion; for x, y ∈ H, the underlying element of x / y in G equals the quotient of the underlying elements.

Русский

Деление в подгруппе соответствует делению в исходной группе через вложение; для x, y ∈ H соответствующий элемент x / y в G равен отношению соответствующих элементов.

LaTeX

$$$$ (x / y)_G = x_G / y_G \\quad (x,y \\in H). $$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_div (x y : H) : (x / y).1 = x.1 / y.1 :=
  rfl

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