coe_inv

Mathlib.Analysis.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.coe_inv

English

The inverse under the coercion corresponds to the inverse in ℂ.

Русский

Обратное через коэрцирование соответствует обратному в ℂ.

LaTeX

$$$$ \\uparrow z^{-1} = (z)^{-1}. $$$$

Lean4

@[simp, norm_cast]
theorem coe_inv (z : Circle) : ↑z⁻¹ = (z : ℂ)⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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