smul_iff — Mathlib

English

IsTrivialBlock is preserved under action by g if and only if g⁻¹ action preserves it, equivalently.

Русский

Сохранение тривиальности блока под действием g эквивалентно сохранению под действием g⁻¹.

LaTeX

$$IsTrivialBlock (g • B) ↔ IsTrivialBlock B$$

Lean4

@[to_additive]
theorem smul_iff {B : Set α} (g : M) : IsTrivialBlock (g • B) ↔ IsTrivialBlock B :=
  by
  constructor
  · intro H
    convert IsTrivialBlock.smul H g⁻¹
    simp only [inv_smul_smul]
  · intro H
    exact IsTrivialBlock.smul H g

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