is_zero_preprimitive — Mathlib

English

Any action is 0-preprimitive; base case for Jordan-style criteria.

Русский

Любое действие является нулевой предпримитивностью; базовый случай для критериев Джордана.

LaTeX

$$IsMultiplyPreprimitive M α 0$$

Lean4

/-- Any action is `0`-preprimitive -/
@[to_additive]
theorem is_zero_preprimitive : IsMultiplyPreprimitive M α 0
    where
  isMultiplyPretransitive := MulAction.is_zero_pretransitive
  isPreprimitive_ofFixingSubgroup hs := by simp at hs

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