smul_mem — Mathlib

English

If r ∈ R and x ∈ skewAdjoint A, then r • x ∈ skewAdjoint A; i.e., the skew-adjoint subset is closed under scalar multiplication.

Русский

Если r ∈ R и x ∈ skewAdjoint A, то r • x ∈ skewAdjoint A; подмножество кососопряжённых элемент закрыто относительно скалярного умножения.

LaTeX

$$$ \\forall r \\in R, \\; \\forall x \\in \\mathrm{skewAdjoint}(A), \\; r \\cdot x \\in \\mathrm{skewAdjoint}(A). $$$

Lean4

@[aesop 90% (rule_sets := [SetLike])]
theorem smul_mem [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A} (h : x ∈ skewAdjoint A) :
    r • x ∈ skewAdjoint A := by rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]

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