one_smul

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.one_smul

English

Unit scalar acts as the identity on a polynomial law: 1•f = f.

Русский

Единица действует как тождественный оператор: 1•f = f.

LaTeX

$$$1\cdot f = f$$$

Lean4

theorem one_smul : (1 : R) • f = f := by ext S; simp only [smul_def, Pi.smul_apply, _root_.one_smul]

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

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

Разделы

Аффилиация

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