map_div_rev

Mathlib.Algebra.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#map_div_rev

English

For a suitable f, f(a/b) = f(b/a).

Русский

Для подходящего отображения f выполняется f(a/b) = f(b/a).

LaTeX

$$$f\left(\frac{a}{b}\right) = f\left(\frac{b}{a}\right)$$$

Lean4

@[to_additive]
theorem map_div_rev : f (x / y) = f (y / x) := by rw [← inv_div, map_inv_eq_map]

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

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

Разделы

Аффилиация

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