apply_one_mul_eq

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Dual.apply_one_mul_eq

← MathLib Explorer

English

For f ∈ Dual R R and r ∈ R, f(1) · r = f(r).

Русский

Для f ∈ Dual R R и r ∈ R выполняется f(1)·r = f(r).

LaTeX

$$$$ f(1) \\cdot r = f(r) \\quad (f \\in \\mathrm{Dual}\\, R\\, R,\\ r \\in R). $$$$

Lean4

@[simp]
theorem apply_one_mul_eq (f : Dual R R) (r : R) : f 1 * r = f r :=
  by
  conv_rhs => rw [← mul_one r, ← smul_eq_mul]
  rw [map_smul, smul_eq_mul, mul_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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