English
Every action is 0-preprimitive; the base case for Jordan-style primitivity results.
Русский
Каждое действие является 0-примитивным; базовый случай для результатов примитивности Джордана.
LaTeX
$$IsMultiplyPreprimitive M α 0$$
Lean4
/-- An `n`-preprimitive action is `m`-preprimitive for `m ≤ n`. -/
@[to_additive /-- An `n`-preprimitive action is `m`-preprimitive for `m ≤ n`. -/
]
theorem isMultiplyPreprimitive_of_le {n : ℕ} (hn : IsMultiplyPreprimitive M α n) {m : ℕ} (hmn : m ≤ n)
(hα : ↑n ≤ ENat.card α) : IsMultiplyPreprimitive M α m := by
induction n with
| zero => rw [Nat.eq_zero_of_le_zero hmn]; exact hn
| succ n hrec =>
rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'
· rw [hmn]; exact hn
· apply hrec (isMultiplyPreprimitive_of_isMultiplyPretransitive_succ M α hα) (Nat.lt_succ_iff.mp hmn')
· refine le_trans ?_ hα; rw [ENat.coe_le_coe]; exact Nat.le_succ n
