hasDiv — Mathlib

English

The quotient of a group by a congruence inherits a division operation: [w] / [y] = [w/y].

Русский

Фактор-группа по конгруэнции наследует операцию деления: [w]/[y] = [w/y].

LaTeX

$$$\\text{Div } c.Quotient$ with $[w]/[y] = [w/y]$$$

Lean4

/-- The division induced on the quotient by a congruence relation on a type with a
division. -/
@[to_additive /-- The subtraction induced on the quotient by an additive congruence relation on a
    type with a subtraction. -/
    ]
instance hasDiv : Div c.Quotient :=
  ⟨(Quotient.map₂ (· / ·)) fun _ _ h₁ _ _ h₂ => c.div h₁ h₂⟩

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