ofLex_div — Mathlib

English

Let α be a type with division. For all a, b in Lex α, the embedding of Lex into α preserves division: ofLex(a/b) = ofLex(a)/ofLex(b).

Русский

Пусть α — множество с операцией деления. Для всех a, b ∈ Lex α отображение ofLex сохраняет операцию деления: ofLex(a/b) = ofLex(a)/ofLex(b).

LaTeX

$$$\operatorname{ofLex}(a/b) = \operatorname{ofLex}(a) / \operatorname{ofLex}(b)$$$

Lean4

@[to_additive (attr := simp)]
theorem ofLex_div [Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b :=
  rfl

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