mk_div

Mathlib.Topology.Algebra.SeparationQuotient.Basic

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.mk_div

English

mk preserves division: mk(x / y) = mk x / mk y.

Русский

mk сохраняет деление: mk(x / y) = mk(x) / mk(y).

LaTeX

$$$\mathrm{mk\_div}: \mathrm{mk}(x/y) = \mathrm{mk}(x)/\mathrm{mk}(y)$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_div [Div G] [ContinuousDiv G] (x y : G) : mk (x / y) = mk x / mk y :=
  rfl

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

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

Разделы

Аффилиация

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