instDiv — Mathlib

English

If G has Div and ContinuousDiv, then SeparationQuotient G has Div.

Русский

Если у G есть деление и непрерывное деление, то SeparationQuotient(G) обладает делением.

LaTeX

$$$\operatorname{Div}(\mathrm{SeparationQuotient}(G))$$$

Lean4

@[to_additive]
instance instDiv [Div G] [ContinuousDiv G] : Div (SeparationQuotient G) where
  div := Quotient.map₂ (· / ·) fun _ _ h₁ _ _ h₂ ↦ (Inseparable.prod h₁ h₂).map continuous_div'

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