div — Mathlib

English

If H is a subgroup of G, then H is closed under the division operation: for any a,b in H, the quotient a/b lies in H.

Русский

Если H является подгруппой G, то она замкнута относительно деления: для любых a,b ∈ H, a/b ∈ H.

LaTeX

$$$H \le G \\Rightarrow \\forall a,b \in H,\\ a/b \in H$$$

Lean4

/-- A subgroup of a group inherits a division -/
@[to_additive /-- An `AddSubgroup` of an `AddGroup` inherits a subtraction. -/
    ]
instance div : Div H :=
  ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩

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