instDivNonemptyInterval — Mathlib

English

There is a division operation on NonemptyInterval(α) when α is a CommGroup with MulLeftMono, defined by s / t = (s.fst / t.snd, s.snd / t.fst).

Русский

Для α, являющегося коммутативной группой с MulLeftMono, существует операция деления на NonemptyInterval(α): s / t = (s.fst / t.snd, s.snd / t.fst).

LaTeX

$$$s / t = (s.fst / t.snd,\; s.snd / t.fst)$$$

Lean4

instance : Div (NonemptyInterval α) :=
  ⟨fun s t => ⟨(s.fst / t.snd, s.snd / t.fst), div_le_div'' s.fst_le_snd t.fst_le_snd⟩⟩

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