English
Under suitable hypotheses (R is a monoid with involutive star, A is a star-module with a unit r), for r self-adjoint and a unit, IsSelfAdjoint(r • x) iff IsSelfAdjoint(x).
Русский
При условии, что R — моноид с инволютивной звездой, A — модуль со звездой, и r — самосопряжённый и единичный, тогда IsSelfAdjoint(r • x) эквивалентно IsSelfAdjoint(x).
LaTeX
$$$IsSelfAdjoint(r) \to IsUnit(r) \to \forall {x}, IsSelfAdjoint(r \cdot x) \leftrightarrow IsSelfAdjoint(x)$$$
Lean4
theorem smul_iff [Monoid R] [StarMul R] [Star A] [MulAction R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r)
(hu : IsUnit r) {x : A} : IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x :=
by
refine ⟨fun hrx ↦ ?_, .smul hr⟩
lift r to Rˣ using hu
rw [← inv_smul_smul r x]
replace hr : IsSelfAdjoint r := Units.ext hr.star_eq
exact hr.inv.smul hrx
