Theorems · Theorem · combinatorics
Fin.isAddFreimanIso_Iio
∀ {k m n : ℕ}, m ≠ 0 → m * k ≤ n → IsAddFreimanIso m (Set.Iio ↑k) (Set.Iio k) Fin.valNo 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.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- AddCommMonoidproof · cited by 12,281
- LE.le.transproof · cited by 3,151
- Nat.cast_oneproof · cited by 2,501
- Set.extproof · cited by 2,266
- Nat.cast_zeroproof · cited by 1,870
- Set.Iiostatement and proof · cited by 1,166
- Set.Iicproof · cited by 1,111
- Nat.cast_addproof · cited by 586
- IsAddFreimanIsostatement and proof · cited by 30
- IsMin.Iio_eqproof · cited by 11
- Fin.val_cast_of_ltproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- Fin.addRothNumber_eq_rothNumberNatproof · cited by 1
- roth_3ap_theorem_natproof · cited by 1
- corners_theorem_natproof · cited by 0