snd_div

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.snd_div

English

The second coordinate of a quotient equals the quotient of the second coordinates: (a/b)_2 = a_2 / b_2.

Русский

Вторая координата частного равна частному вторых координат: (a/b)_2 = a_2 / b_2.

LaTeX

$$(a/b)_2 = a_2 / b_2$$

Lean4

@[to_additive (attr := simp)]
theorem snd_div (a b : G × H) : (a / b).2 = a.2 / b.2 :=
  rfl

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

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

Разделы

Аффилиация

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