smul — Mathlib

English

If B is a trivial block and g ∈ M, then g • B is also a trivial block.

Русский

Если B — простой блок и $g$ действует, то $g \\cdot B$ тоже простой блок.

LaTeX

$$IsTrivialBlock B → IsTrivialBlock (g • B)$$

Lean4

@[to_additive]
theorem smul {B : Set α} (hB : IsTrivialBlock B) (g : M) : IsTrivialBlock (g • B) := by
  cases hB with
  | inl h =>
    left
    exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h
  | inr h =>
    right
    rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

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