mod_get_eq — Mathlib

English

Let a,b be parts of α with Dom(a % b). Then the value of (a % b) equals the mod of the values a and b taken at their respective domains.

Русский

Пусть a,b — части α с Dom(a % b). Тогда значение (a % b) равно модулю значений a и b взятых в их соответствующих доменах.

LaTeX

$$$$ (a \bmod b).get(hab) = a.get(left\_dom\_of\_mod\_dom(hab)) \bmod b.get(right\_dom\_of\_mod\_dom(hab)). $$$$

Lean4

@[simp]
theorem mod_get_eq [Mod α] (a b : Part α) (hab : Dom (a % b)) :
    (a % b).get hab = a.get (left_dom_of_mod_dom hab) % b.get (right_dom_of_mod_dom hab) := by simp [mod_def]; aesop

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