skewMonoidAlgebra_iff — Mathlib

English

For a, IsSMulRegular k a holds if and only if IsSMulRegular (SkewMonoidAlgebra k G) a, assuming [Nonempty G].

Русский

Для любого a выполняется: IsSMulRegular k a тогда и только тогда, когда IsSMulRegular (SkewMonoidAlgebra k G) a, при условии Nonempty G.

LaTeX

$$$\\text{IsSMulRegular}\\ k\ \ a \iff \\text{IsSMulRegular}\\ (SkewMonoidAlgebra\\ k\\ G)\\ a$$$

Lean4

theorem _root_.IsSMulRegular.skewMonoidAlgebra_iff {S : Type*} [Monoid S] [DistribMulAction S k] {a : S} [Nonempty G] :
    IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a :=
  by
  inhabit G
  refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩
  rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj
  exact single_injective (default) (ha inj)

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