map_div₀

Mathlib.Algebra.GroupWithZero.Units.Lemmas

URI: https://scilib.ai/kg/mathlib#map_div₀

English

The map preserves division: f(a / b) = f(a) / f(b).

Русский

Отображение сохраняет деление: f(a / b) = f(a) / f(b).

LaTeX

$$$f(a / b) = f(a) / f(b)$$$

Lean4

@[simp]
theorem map_div₀ : f (a / b) = f a / f b :=
  map_div' f (map_inv₀ f) a b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru