English
Let e be a bijection between types α and β. If M acts centrally on β, then α also carries a central scalar action obtained by transporting the action along e.
Русский
Пусть e — биекция между множествами α и β. Если на β действуют скаляры M центрально, то и на α действует центральное скалярное действие, полученное переносом действия через e.
LaTeX
$$$\\forall e:\\alpha \\simeq \\beta,\\ \\operatorname{IsCentralScalar} M \\beta \\Rightarrow \\operatorname{IsCentralScalar} M \\alpha$$$
Lean4
/-- Transfer `IsCentralScalar` across an `Equiv` -/
@[to_additive /-- Transfer `IsCentralVAdd` across an `Equiv` -/
]
protected theorem isCentralScalar (e : α ≃ β) [IsCentralScalar M β] :
letI := e.smul M
letI := e.smul Mᵐᵒᵖ
IsCentralScalar M α :=
letI := e.smul M
letI := e.smul Mᵐᵒᵖ
{ op_smul_eq_smul := by simp [smul_def, op_smul_eq_smul] }
