English
A similar no-wrap Freiman isomorphism for Iio: if hm ≠ 0 and hkmn ≤ n, then IsAddFreimanIso m (Iio k) (Iio k) Fin.val.
Русский
Аналогично без оберток: IsAddFreimanIso m на Iio k.
LaTeX
$$$IsAddFreimanIso m (Iio k) (Iio k) Fin.val$$$
Lean4
/-- **No wrap-around principle**.
The first `k` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k` elements of `ℕ`
assuming there is no wrap-around. -/
theorem isAddFreimanIso_Iio (hm : m ≠ 0) (hkmn : m * k ≤ n) : IsAddFreimanIso m (Iio (k : Fin (n + 1))) (Iio k) val :=
by
obtain _ | k := k
· simp [← bot_eq_zero]
have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn
convert isAddFreimanIso_Iic hm hkmn' using 1 <;> ext x
· simp [lt_iff_val_lt_val, le_iff_val_le_val, -val_fin_le, -val_fin_lt, Nat.mod_eq_of_lt, aux hm hkmn']
simp_rw [← Nat.cast_add_one]
rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]
· simp [Nat.lt_succ_iff]
