some_div_some — Mathlib

English

Let α be a type with a binary division. The embedding a ↦ some(a) preserves division, i.e. for all a,b ∈ α, some(a) divided by some(b) equals some(a divided by b).

Русский

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

LaTeX

$$$$\forall a,b \in \alpha,\ \mathrm{some}(a) / \mathrm{some}(b) = \mathrm{some}(a / b).$$$$

Lean4

@[to_additive]
theorem some_div_some [Div α] (a b : α) : some a / some b = some (a / b) := by simp [div_def]

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