div — Mathlib

English

An equivalence e : α ≃ β transfers division from β to α by defining x/y := e^{-1}(e x / e y).

Русский

Эквивалентность e : α ≃ β переносит деление с β на α через определение x/y := e^{-1}(e x / e y).

LaTeX

$$$$\frac{x}{y} = e^{-1}\left(\frac{e x}{e y}\right).$$$$

Lean4

/-- Transfer `Div` across an `Equiv` -/
@[to_additive /-- Transfer `Sub` across an `Equiv` -/
    ]
protected abbrev div [Div β] : Div α :=
  ⟨fun x y => e.symm (e x / e y)⟩

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