equiv_apply

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#PerfectionMap.equiv_apply

English

If m ≤ n and coeff m ≠ 0, then coeff n ≠ 0.

Русский

Если m ≤ n и coeff m ≠ 0, тогда coeff n ≠ 0.

LaTeX

$$$\\Big(\\operatorname{coeff} R p m f \\neq 0\\Big) \\land (m \\le n) \\Rightarrow \\operatorname{coeff} R p n f \\neq 0$$$

Lean4

theorem equiv_apply {π : P →+* R} (m : PerfectionMap p π) (x : P) : m.equiv x = Perfection.lift p P R π x :=
  rfl

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

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

Разделы

Аффилиация

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