fin n
is the subtype of ℕ
consisting of natural numbers strictly smaller than n
.
Instances for fin
- slim_check.fin.sampleable'
- fin.has_lt
- fin.has_le
- fin.has_repr
- fin.has_to_string
- fin.has_zero
- fin.has_one
- fin.has_add
- fin.has_sub
- fin.has_mul
- fin.has_mod
- fin.has_div
- fin.is_empty
- fin.inhabited
- inhabited_fin_one_add
- fin.unique
- fin.fin_to_nat
- fin.linear_order
- fin.partial_order
- fin.fin.lt.is_well_order
- fin.has_well_founded
- fin.bounded_order
- fin.lattice
- fin.nontrivial
- fin.add_comm_monoid
- fin.add_monoid_with_one
- fin.has_neg
- fin.add_comm_group
- fin.reflect
- fin.fintype
- fin.countable
- fin.encodable
- subsingleton_fin_zero
- subsingleton_fin_one
- fin.locally_finite_order
- fin.locally_finite_order_bot
- fin.locally_finite_order_top
- fin.comm_semigroup
- fin.comm_ring
- category_theory.fin_category.category_as_type
- category_theory.fin_category.as_type_fin_category
- fin.complete_linear_order
- fin.nonempty_fin_lin_ord
- fin.succ_order
- fin.pred_order
- primcodable.fin
- fin_random
- fin_bounded_random
- fin_enum.fin
- fin.non_null_json_serializable
- fin.has_variable_names
- slim_check.fin.sampleable
@[protected, instance]
Equations
- fin.has_lt = {lt := fin.lt n}
@[protected, instance]
Equations
- fin.has_le = {le := fin.le n}
@[protected, instance]
Equations
- a.decidable_lt b = a.val.decidable_lt b.val
@[protected, instance]
Equations
- a.decidable_le b = a.val.decidable_le b.val
@[protected, instance]
Equations
- fin.decidable_eq n = λ (i j : fin n), decidable_of_decidable_of_iff (nat.decidable_eq i.val j.val) _