ofFixingSubgroup — Mathlib

English

The carrier of the SubMulAction of fixingSubgroup on the complement is precisely the complement of the fixed set.

Русский

Множество переносимой подгруппы фиксирования на дополнении равно дополнению фиксированного множества.

LaTeX

$$carrier(ofFixingSubgroup M s) = sᶜ$$

Lean4

/-- The `SubMulAction` of `fixingSubgroup M s` on the complement of `s`. -/
@[to_additive /-- The `SubAddAction` of `fixingAddSubgroup M s` on the complement of `s`. -/
    ]
def ofFixingSubgroup : SubMulAction (fixingSubgroup M s) α
    where
  carrier := sᶜ
  smul_mem' := fun ⟨c, hc⟩ x ↦ by
    rw [← Subgroup.inv_mem_iff] at hc
    simp only [Set.mem_compl_iff, not_imp_not]
    intro hcx
    rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]

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