toCircle_add — Mathlib

English

The toCircle map respects addition: toCircle(x + y) = toCircle x · toCircle y.

Русский

Отображение toCircle сохраняет сложение: toCircle(x + y) = toCircle x · toCircle y.

LaTeX

$$$$ toCircle(x + y) = toCircle(x) \cdot toCircle(y). $$$$

Lean4

theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : @toCircle T (x + y) = toCircle x * toCircle y :=
  by
  induction x using QuotientAddGroup.induction_on
  induction y using QuotientAddGroup.induction_on
  simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]

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