fixedBy_mul — Mathlib

English

If an element is fixed by m1 and fixed by m2, then it is fixed by m1 m2: fixedBy α m1 ∩ fixedBy α m2 ⊆ fixedBy α (m1 m2).

Русский

Если точка зафиксирована m1 и m2, то она фиксируется и m1 m2: фиксированные точки m1 ∩ фиксированные точки m2 ⊆ фиксированные точки m1 m2.

LaTeX

$$$ fixedBy(α, m1) \cap fixedBy(α, m2) \subseteq fixedBy(α, m1 m2) $$$

Lean4

@[to_additive]
theorem fixedBy_mul (m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂) :=
  by
  intro a ⟨h₁, h₂⟩
  rw [mem_fixedBy, mul_smul, h₂, h₁]

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