isRestricted_iff_abs

Mathlib.RingTheory.PowerSeries.Restricted

URI: https://scilib.ai/kg/mathlib#PowerSeries.IsRestricted.isRestricted_iff_abs

English

IsRestricted c f is equivalent to IsRestricted |c| f.

Русский

IsRestricted c f эквивалентно IsRestricted |c| f.

LaTeX

$$$\mathrm{IsRestricted}(c,f) \iff \mathrm{IsRestricted}(|c|, f)$$$

Lean4

theorem isRestricted_iff_abs (f : PowerSeries R) : IsRestricted c f ↔ IsRestricted |c| f := by simp [isRestricted_iff]

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

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

Разделы

Аффилиация

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