smul_def

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.smul_def

English

The action of AlgEquiv on A1 satisfies f • a = f(a).

Русский

Действие AlgEquiv на A1 удовлетворяет f • a = f(a).

LaTeX

$$$ f \\cdot a = f(a) $$$

Lean4

@[simp]
protected theorem smul_def (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a :=
  rfl

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

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

Разделы

Аффилиация

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