circleEquivGen_symm_apply

Mathlib.NumberTheory.PythagoreanTriples

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

← MathLib Explorer

English

The symm_apply form gives that the inverse image is v1/(v2+1).

Русский

Обратное отображение равно v1/(v2+1).

LaTeX

$$\forall v,_circleEquivGen hk .symm v = v.fst / (v.snd + 1)$$

Lean4

@[simp]
theorem circleEquivGen_symm_apply (hk : ∀ x : K, 1 + x ^ 2 ≠ 0)
    (v : { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) :
    (circleEquivGen hk).symm v = (v : K × K).1 / ((v : K × K).2 + 1) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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