smulOfUnit

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.smulOfUnit

← MathLib Explorer

English

Multiplication by a unit a ∈ R^× gives a linear equivalence M ≃ M.

Русский

Умножение на единицу-кратное число a ∈ R^× задаёт линейное эквив between M и itself.

LaTeX

$$$\mathrm{smulOfUnit}(a) : M \simeq M$$$

Lean4

/-- Multiplying by a unit `a` of the ring `R` is a linear equivalence. -/
def smulOfUnit (a : Rˣ) : M ≃ₗ[R] M :=
  DistribMulAction.toLinearEquiv R M a

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

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

Разделы

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

Аффилиация

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