The finite type with n
elements #
Fin n
is the type whose elements are natural numbers smaller than n
.
This file expands on the development in the core library.
Main definitions #
Induction principles #
finZeroElim
: Elimination principle for the empty setFin 0
, generalizesFin.elim0
. Further definitions and eliminators can be found inInit.Data.Fin.Lemmas
Embeddings and isomorphisms #
Fin.valEmbedding
: coercion to natural numbers as anEmbedding
;Fin.succEmb
:Fin.succ
as anEmbedding
;Fin.castLEEmb h
:Fin.castLE
as anEmbedding
, embedFin n
intoFin m
,h : n ≤ m
;finCongr
:Fin.cast
as anEquiv
, equivalence betweenFin n
andFin m
whenn = m
;Fin.castAddEmb m
:Fin.castAdd
as anEmbedding
, embedFin n
intoFin (n+m)
;Fin.castSuccEmb
:Fin.castSucc
as anEmbedding
, embedFin n
intoFin (n+1)
;Fin.addNatEmb m i
:Fin.addNat
as anEmbedding
, addm
oni
on the right, generalizesFin.succ
;Fin.natAddEmb n i
:Fin.natAdd
as anEmbedding
, addsn
oni
on the left;
Other casts #
Fin.divNat i
: dividesi : Fin (m * n)
byn
;Fin.modNat i
: takes the mod ofi : Fin (m * n)
byn
;
Elimination principle for the empty set Fin 0
, dependent version.
Equations
- finZeroElim x = x.elim0
Instances For
coercions and constructions #
order #
The inclusion map Fin n → ℕ
is an embedding.
Equations
- Fin.valEmbedding = { toFun := Fin.val, inj' := ⋯ }
Instances For
Use the ordering on Fin n
for checking recursive definitions.
For example, the following definition is not accepted by the termination checker,
unless we declare the WellFoundedRelation
instance:
def factorial {n : ℕ} : Fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
Alias of Fin.val_zero
.
Fin.mk_zero
in Lean
only applies in Fin (n + 1)
.
This one instead uses a NeZero n
typeclass hypothesis.
The Fin.zero_le
in Lean
only applies in Fin (n+1)
.
This one instead uses a NeZero n
typeclass hypothesis.
Coercions to ℤ
and the fin_omega
tactic. #
Preprocessor for omega
to handle inequalities in Fin
.
Note that this involves a lot of case splitting, so may be slow.
Equations
- Fin.tacticFin_omega = Lean.ParserDescr.node `Fin.tacticFin_omega 1024 (Lean.ParserDescr.nonReservedSymbol "fin_omega" false)
Instances For
addition, numerals, and coercion from Nat #
Equations
Equations
- Fin.instNatCast = { natCast := fun (i : ℕ) => Fin.ofNat' n i }
succ and casts into larger Fin types #
Alias of Fin.coe_succEmb
.
The Fin.succ_one_eq_two
in Lean
only applies in Fin (n+2)
.
This one instead uses a NeZero n
typeclass hypothesis.
Fin.castLE
as an Embedding
, castLEEmb h i
embeds i
into a larger Fin
type.
Equations
- Fin.castLEEmb h = { toFun := Fin.castLE h, inj' := ⋯ }
Instances For
While in many cases finCongr
is better than Equiv.cast
/cast
, sometimes we want to apply
a generic theorem about cast
.
Fin.castAdd
as an Embedding
, castAddEmb m i
embeds i : Fin n
in Fin (n+m)
.
See also Fin.natAddEmb
and Fin.addNatEmb
.
Equations
Instances For
The Fin.castSucc_zero
in Lean
only applies in Fin (n+1)
.
This one instead uses a NeZero n
typeclass hypothesis.
Fin.addNat
as an Embedding
, addNatEmb m i
adds m
to i
, generalizes Fin.succ
.
Equations
- Fin.addNatEmb m = { toFun := fun (x : Fin n) => x.addNat m, inj' := ⋯ }
Instances For
Fin.natAdd
as an Embedding
, natAddEmb n i
adds n
to i
"on the left".
Equations
- Fin.natAddEmb n = { toFun := Fin.natAdd n, inj' := ⋯ }
Instances For
pred #
Fin.succAbove p
as an Embedding
.
Equations
- p.succAboveEmb = { toFun := p.succAbove, inj' := ⋯ }
Instances For
succAbove
is injective at the pivot
By moving succ
to the outside of this expression, we create opportunities for further
simplification using succAbove_zero
or succ_succAbove_zero
.
recursion and induction principles #
Alias of Fin.eq_one_of_ne_zero
.