Documentation

Mathlib.Data.Fin.Basic

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 #

Order embeddings and an order isomorphism #

Other casts #

Misc definitions #

def finZeroElim {α : Fin 0Sort u_1} (x : Fin 0) :
α x

Elimination principle for the empty set Fin 0, dependent version.

Equations
Instances For
    instance Fin.instCanLiftNatFinValLtInstLTNat {n : } :
    CanLift (Fin n) Fin.val fun (x : ) => x < n
    Equations
    • =
    def Fin.rec0 {α : Fin 0Sort u_1} (i : Fin 0) :
    α i

    A dependent variant of Fin.elim0.

    Equations
    Instances For
      theorem Fin.size_positive {n : } :
      Fin n0 < n

      If you actually have an element of Fin n, then the n is always positive

      theorem Fin.size_positive' {n : } [Nonempty (Fin n)] :
      0 < n
      theorem Fin.prop {n : } (a : Fin n) :
      a < n
      @[simp]
      theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
      Fin.equivSubtype a = { val := a, property := }
      @[simp]
      theorem Fin.equivSubtype_symm_apply {n : } (a : { i : // i < n }) :
      Fin.equivSubtype.symm a = { val := a, isLt := }
      def Fin.equivSubtype {n : } :
      Fin n { i : // i < n }

      Equivalence between Fin n and { i // i < n }.

      Equations
      • Fin.equivSubtype = { toFun := fun (a : Fin n) => { val := a, property := }, invFun := fun (a : { i : // i < n }) => { val := a, isLt := }, left_inv := , right_inv := }
      Instances For

        coercions and constructions #

        theorem Fin.val_eq_val {n : } (a : Fin n) (b : Fin n) :
        a = b a = b
        @[deprecated Fin.ext_iff]
        theorem Fin.eq_iff_veq {n : } (a : Fin n) (b : Fin n) :
        a = b a = b
        theorem Fin.ne_iff_vne {n : } (a : Fin n) (b : Fin n) :
        a b a b
        @[simp]
        theorem Fin.mk_eq_mk {n : } {a : } {h : a < n} {a' : } {h' : a' < n} :
        { val := a, isLt := h } = { val := a', isLt := h' } a = a'
        theorem Fin.heq_fun_iff {α : Sort u_1} {k : } {l : } (h : k = l) {f : Fin kα} {g : Fin lα} :
        HEq f g ∀ (i : Fin k), f i = g { val := i, isLt := }

        Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

        theorem Fin.heq_fun₂_iff {α : Sort u_1} {k : } {l : } {k' : } {l' : } (h : k = l) (h' : k' = l') {f : Fin kFin k'α} {g : Fin lFin l'α} :
        HEq f g ∀ (i : Fin k) (j : Fin k'), f i j = g { val := i, isLt := } { val := j, isLt := }

        Assume k = l and k' = l'. If two functions Fin k → Fin k' → α and Fin l → Fin l' → α are equal on each pair, then they coincide (in the heq sense).

        theorem Fin.heq_ext_iff {k : } {l : } (h : k = l) {i : Fin k} {j : Fin l} :
        HEq i j i = j

        order #

        theorem Fin.le_iff_val_le_val {n : } {a : Fin n} {b : Fin n} :
        a b a b
        @[simp]
        theorem Fin.val_fin_lt {n : } {a : Fin n} {b : Fin n} :
        a < b a < b

        a < b as natural numbers if and only if a < b in Fin n.

        @[simp]
        theorem Fin.val_fin_le {n : } {a : Fin n} {b : Fin n} :
        a b a b

        a ≤ b as natural numbers if and only if a ≤ b in Fin n.

        Equations
        theorem Fin.min_val {n : } {a : Fin n} :
        min (a) n = a
        theorem Fin.max_val {n : } {a : Fin n} :
        max (a) n = n
        Equations
        • Fin.instPartialOrderFin = inferInstance
        theorem Fin.val_strictMono {n : } :
        StrictMono Fin.val
        @[simp]
        theorem Fin.orderIsoSubtype_apply {n : } (a : Fin n) :
        Fin.orderIsoSubtype a = { val := a, property := }
        @[simp]
        theorem Fin.orderIsoSubtype_symm_apply {n : } (a : { i : // i < n }) :
        (RelIso.symm Fin.orderIsoSubtype) a = { val := a, isLt := }
        def Fin.orderIsoSubtype {n : } :
        Fin n ≃o { i : // i < n }

        The equivalence Fin n ≃ { i // i < n } is an order isomorphism.

        Equations
        Instances For
          @[simp]
          theorem Fin.valEmbedding_apply {n : } (self : Fin n) :
          Fin.valEmbedding self = self

          The inclusion map Fin n → ℕ is an embedding.

          Equations
          • Fin.valEmbedding = { toFun := Fin.val, inj' := }
          Instances For
            @[simp]
            theorem Fin.equivSubtype_symm_trans_valEmbedding {n : } :
            Function.Embedding.trans (Equiv.toEmbedding Fin.equivSubtype.symm) Fin.valEmbedding = Function.Embedding.subtype fun (x : ) => x < n
            @[simp]
            theorem Fin.valOrderEmbedding_apply (n : ) (self : Fin n) :
            (Fin.valOrderEmbedding n) self = self

            The inclusion map Fin n → ℕ is an order embedding.

            Equations
            Instances For
              instance Fin.Lt.isWellOrder (n : ) :
              IsWellOrder (Fin n) fun (x x_1 : Fin n) => x < x_1

              The ordering on Fin n is a well order.

              Equations
              • =

              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⟩
              
              Equations
              • Fin.instWellFoundedRelationFin = measure Fin.val
              def Fin.ofNat'' {n : } [NeZero n] (i : ) :
              Fin n

              Given a positive n, Fin.ofNat' i is i % n as an element of Fin n.

              Equations
              Instances For
                instance Fin.instZeroFin {n : } [NeZero n] :
                Zero (Fin n)
                Equations
                instance Fin.instOneFin {n : } [NeZero n] :
                One (Fin n)
                Equations
                @[simp]
                theorem Fin.val_zero' (n : ) [NeZero n] :
                0 = 0

                The Fin.val_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                @[simp]
                theorem Fin.zero_le' {n : } [NeZero n] (a : Fin n) :
                0 a

                The Fin.zero_le in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                theorem Fin.pos_iff_ne_zero' {n : } [NeZero n] (a : Fin n) :
                0 < a a 0

                The Fin.pos_iff_ne_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                @[simp]
                theorem Fin.cast_eq_self {n : } (a : Fin n) :
                Fin.cast a = a
                @[simp]
                theorem Fin.revPerm_symm_apply {n : } (i : Fin n) :
                Fin.revPerm.symm i = Fin.rev i
                @[simp]
                theorem Fin.revPerm_apply {n : } (i : Fin n) :
                Fin.revPerm i = Fin.rev i
                def Fin.revPerm {n : } :

                Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by i ↦ n-(i+1).

                Equations
                Instances For
                  @[simp]
                  theorem Fin.revPerm_symm {n : } :
                  Fin.revPerm.symm = Fin.revPerm
                  @[simp]
                  theorem Fin.revOrderIso_apply {n : } :
                  ∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = Fin.rev (OrderDual.ofDual a)
                  @[simp]
                  theorem Fin.revOrderIso_toEquiv {n : } :
                  Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm

                  Fin.rev n as an order-reversing isomorphism.

                  Equations
                  • Fin.revOrderIso = { toEquiv := OrderDual.ofDual.trans Fin.revPerm, map_rel_iff' := }
                  Instances For
                    @[simp]
                    theorem Fin.revOrderIso_symm_apply {n : } (i : Fin n) :
                    (OrderIso.symm Fin.revOrderIso) i = OrderDual.toDual (Fin.rev i)
                    theorem Fin.cast_rev {n : } {m : } (i : Fin n) (h : n = m) :
                    theorem Fin.rev_eq_iff {n : } {i : Fin n} {j : Fin n} :
                    theorem Fin.rev_ne_iff {n : } {i : Fin n} {j : Fin n} :
                    theorem Fin.rev_lt_iff {n : } {i : Fin n} {j : Fin n} :
                    theorem Fin.rev_le_iff {n : } {i : Fin n} {j : Fin n} :
                    theorem Fin.lt_rev_iff {n : } {i : Fin n} {j : Fin n} :
                    theorem Fin.le_rev_iff {n : } {i : Fin n} {j : Fin n} :
                    Equations
                    • Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin = BoundedOrder.mk
                    Equations
                    • Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat = LinearOrder.toLattice
                    theorem Fin.last_pos' {n : } [NeZero n] :
                    theorem Fin.one_lt_last {n : } [NeZero n] :
                    1 < Fin.last (n + 1)
                    theorem Fin.bot_eq_zero (n : ) :
                    = 0
                    @[simp]
                    theorem Fin.coe_orderIso_apply {n : } {m : } (e : Fin n ≃o Fin m) (i : Fin n) :
                    (e i) = i

                    If e is an orderIso between Fin n and Fin m, then n = m and e is the identity map. In this lemma we state that for each i : Fin n we have (e i : ℕ) = (i : ℕ).

                    instance Fin.orderIso_subsingleton {n : } {α : Type u_1} [Preorder α] :
                    Equations
                    • =
                    instance Fin.orderIso_subsingleton' {n : } {α : Type u_1} [Preorder α] :
                    Equations
                    • =
                    instance Fin.orderIsoUnique {n : } :
                    Equations
                    theorem Fin.strictMono_unique {n : } {α : Type u_1} [Preorder α] {f : Fin nα} {g : Fin nα} (hf : StrictMono f) (hg : StrictMono g) (h : Set.range f = Set.range g) :
                    f = g

                    Two strictly monotone functions from Fin n are equal provided that their ranges are equal.

                    theorem Fin.orderEmbedding_eq {n : } {α : Type u_1} [Preorder α] {f : Fin n ↪o α} {g : Fin n ↪o α} (h : Set.range f = Set.range g) :
                    f = g

                    Two order embeddings of Fin n are equal provided that their ranges are equal.

                    addition, numerals, and coercion from Nat #

                    @[simp]
                    theorem Fin.val_one' (n : ) [NeZero n] :
                    1 = 1 % n
                    theorem Fin.val_one'' {n : } :
                    1 = 1 % (n + 1)
                    instance Fin.nontrivial {n : } :
                    Nontrivial (Fin (n + 2))
                    Equations
                    • =
                    theorem Fin.add_zero {n : } [NeZero n] (k : Fin n) :
                    k + 0 = k
                    theorem Fin.zero_add {n : } [NeZero n] (k : Fin n) :
                    0 + k = k
                    instance Fin.instOfNatFin {n : } {a : } [NeZero n] :
                    OfNat (Fin n) a
                    Equations
                    instance Fin.inhabited (n : ) [NeZero n] :
                    Equations
                    instance Fin.inhabitedFinOneAdd (n : ) :
                    Inhabited (Fin (1 + n))
                    Equations
                    @[simp]
                    theorem Fin.default_eq_zero (n : ) [NeZero n] :
                    default = 0
                    @[simp]
                    theorem Fin.ofNat'_zero {n : } {h : n > 0} [NeZero n] :
                    @[simp]
                    theorem Fin.ofNat'_one {n : } {h : n > 0} [NeZero n] :
                    theorem Fin.val_add_eq_ite {n : } (a : Fin n) (b : Fin n) :
                    (a + b) = if n a + b then a + b - n else a + b
                    @[deprecated]
                    theorem Fin.val_bit0 {n : } (k : Fin n) :
                    (bit0 k) = bit0 k % n
                    @[deprecated]
                    theorem Fin.val_bit1 {n : } [NeZero n] (k : Fin n) :
                    (bit1 k) = bit1 k % n
                    @[simp, deprecated]
                    theorem Fin.mk_bit0 {m : } {n : } (h : bit0 m < n) :
                    { val := bit0 m, isLt := h } = bit0 { val := m, isLt := }
                    @[simp, deprecated]
                    theorem Fin.mk_bit1 {m : } {n : } [NeZero n] (h : bit1 m < n) :
                    { val := bit1 m, isLt := h } = bit1 { val := m, isLt := }
                    @[simp]
                    theorem Fin.ofNat''_eq_cast (n : ) [NeZero n] (a : ) :
                    Fin.ofNat'' a = a
                    @[simp]
                    theorem Fin.val_nat_cast (a : ) (n : ) [NeZero n] :
                    a = a % n
                    theorem Fin.val_cast_of_lt {n : } [NeZero n] {a : } (h : a < n) :
                    a = a

                    Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

                    @[simp]
                    theorem Fin.cast_val_eq_self {n : } [NeZero n] (a : Fin n) :
                    a = a

                    If n is non-zero, converting the value of a Fin n to Fin n results in the same value.

                    @[simp]
                    theorem Fin.nat_cast_self (n : ) [NeZero n] :
                    n = 0
                    @[simp]
                    theorem Fin.nat_cast_eq_zero {a : } {n : } [NeZero n] :
                    a = 0 n a
                    @[simp]
                    theorem Fin.cast_nat_eq_last (n : ) :
                    n = Fin.last n
                    theorem Fin.le_val_last {n : } (i : Fin (n + 1)) :
                    i n
                    @[simp]
                    theorem Fin.one_eq_zero_iff {n : } [NeZero n] :
                    1 = 0 n = 1
                    @[simp]
                    theorem Fin.zero_eq_one_iff {n : } [NeZero n] :
                    0 = 1 n = 1

                    succ and casts into larger Fin types #

                    theorem Fin.strictMono_succ {n : } :
                    StrictMono Fin.succ
                    def Fin.succEmb (n : ) :
                    Fin n ↪o Fin (n + 1)

                    Fin.succ as an OrderEmbedding

                    Equations
                    Instances For
                      @[simp]
                      theorem Fin.val_succEmb {n : } :
                      (Fin.succEmb n) = Fin.succ
                      @[simp]
                      theorem Fin.exists_succ_eq {n : } {x : Fin (n + 1)} :
                      (∃ (y : Fin n), Fin.succ y = x) x 0
                      theorem Fin.exists_succ_eq_of_ne_zero {n : } {x : Fin (n + 1)} (h : x 0) :
                      ∃ (y : Fin n), Fin.succ y = x
                      @[simp]
                      theorem Fin.succ_zero_eq_one' {n : } [NeZero n] :
                      theorem Fin.one_pos' {n : } [NeZero n] :
                      0 < 1
                      theorem Fin.zero_ne_one' {n : } [NeZero n] :
                      0 1
                      @[simp]
                      theorem Fin.succ_one_eq_two' {n : } [NeZero n] :

                      The Fin.succ_one_eq_two in Std only applies in Fin (n+2). This one instead uses a NeZero n typeclass hypothesis.

                      @[simp]
                      theorem Fin.le_zero_iff' {n : } [NeZero n] {k : Fin n} :
                      k 0 k = 0

                      The Fin.le_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                      @[simp]
                      theorem Fin.cast_refl {n : } (h : n = n) :
                      Fin.cast h = id
                      theorem Fin.strictMono_castLE {n : } {m : } (h : n m) :
                      theorem Fin.castLE_injective {n : } {m : } (hmn : m n) :
                      @[simp]
                      theorem Fin.castLE_inj {n : } {m : } {hmn : m n} {a : Fin m} {b : Fin m} :
                      Fin.castLE hmn a = Fin.castLE hmn b a = b
                      @[simp]
                      theorem Fin.castLEEmb_toEmbedding {n : } {m : } (h : n m) :
                      (Fin.castLEEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := }
                      @[simp]
                      theorem Fin.castLEEmb_apply {n : } {m : } (h : n m) (i : Fin n) :
                      def Fin.castLEEmb {n : } {m : } (h : n m) :

                      Fin.castLE as an OrderEmbedding, castLEEmb h i embeds i into a larger Fin type.

                      Equations
                      Instances For
                        theorem Fin.equiv_iff_eq {n : } {m : } :
                        Nonempty (Fin m Fin n) m = n
                        @[simp]
                        theorem Fin.castLE_castSucc {n : } {m : } (i : Fin n) (h : n + 1 m) :
                        @[simp]
                        theorem Fin.castLE_comp_castSucc {n : } {m : } (h : n + 1 m) :
                        Fin.castLE h Fin.castSucc = Fin.castLE
                        @[simp]
                        theorem Fin.castLE_rfl (n : ) :
                        Fin.castLE = id
                        @[simp]
                        theorem Fin.range_castLE {n : } {k : } (h : n k) :
                        Set.range (Fin.castLE h) = {i : Fin k | i < n}
                        @[simp]
                        theorem Fin.coe_of_injective_castLEEmb_symm {n : } {k : } (h : n k) (i : Fin k) (hi : i Set.range (Fin.castLEEmb h)) :
                        ((Equiv.ofInjective (Fin.castLEEmb h) ).symm { val := i, property := hi }) = i
                        theorem Fin.leftInverse_cast {n : } {m : } (eq : n = m) :
                        theorem Fin.rightInverse_cast {n : } {m : } (eq : n = m) :
                        theorem Fin.cast_le_cast {n : } {m : } (eq : n = m) {a : Fin n} {b : Fin n} :
                        Fin.cast eq a Fin.cast eq b a b
                        @[simp]
                        theorem Fin.castIso_apply {n : } {m : } (eq : n = m) (i : Fin n) :
                        (Fin.castIso eq) i = Fin.cast eq i
                        @[simp]
                        theorem Fin.castIso_symm_apply {n : } {m : } (eq : n = m) (i : Fin m) :
                        def Fin.castIso {n : } {m : } (eq : n = m) :

                        Fin.cast as an OrderIso, castIso eq i embeds i into an equal Fin type, see also Equiv.finCongr.

                        Equations
                        Instances For
                          @[simp]
                          theorem Fin.symm_castIso {n : } {m : } (h : n = m) :
                          @[simp]
                          theorem Fin.cast_zero {n : } {n' : } [NeZero n] {h : n = n'} :
                          Fin.cast h 0 = 0
                          @[simp]
                          theorem Fin.castIso_refl {n : } (h : optParam (n = n) ) :
                          theorem Fin.castIso_to_equiv {n : } {m : } (h : n = m) :
                          (Fin.castIso h).toEquiv = Equiv.cast

                          While in many cases Fin.castIso is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

                          theorem Fin.cast_eq_cast {n : } {m : } (h : n = m) :

                          While in many cases Fin.cast is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

                          @[simp]
                          theorem Fin.castAddEmb_apply {n : } (m : ) :
                          ∀ (a : Fin n), (Fin.castAddEmb m) a = Fin.castAdd m a
                          @[simp]
                          theorem Fin.castAddEmb_toEmbedding {n : } (m : ) :
                          (Fin.castAddEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := }
                          def Fin.castAddEmb {n : } (m : ) :
                          Fin n ↪o Fin (n + m)

                          Fin.castAdd as an OrderEmbedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

                          Equations
                          Instances For
                            theorem Fin.strictMono_castSucc {n : } :
                            StrictMono Fin.castSucc
                            @[simp]
                            theorem Fin.castSuccEmb_apply {n : } :
                            ∀ (a : Fin n), Fin.castSuccEmb a = Fin.castSucc a
                            @[simp]
                            theorem Fin.castSuccEmb_toEmbedding {n : } :
                            Fin.castSuccEmb.toEmbedding = { toFun := Fin.castSucc, inj' := }
                            def Fin.castSuccEmb {n : } :
                            Fin n ↪o Fin (n + 1)

                            Fin.castSucc as an OrderEmbedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

                            Equations
                            Instances For
                              @[simp]
                              theorem Fin.castSucc_le_castSucc_iff :
                              ∀ {n : } {a b : Fin n}, Fin.castSucc a Fin.castSucc b a b
                              @[simp]
                              theorem Fin.succ_le_castSucc_iff :
                              ∀ {n : } {a b : Fin n}, Fin.succ a Fin.castSucc b a < b
                              @[simp]
                              theorem Fin.castSucc_lt_succ_iff :
                              ∀ {n : } {a b : Fin n}, Fin.castSucc a < Fin.succ b a b
                              theorem Fin.le_of_castSucc_lt_of_succ_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} {i : Fin n} (hl : Fin.castSucc i < a) (hu : b < Fin.succ i) :
                              b < a
                              theorem Fin.castSucc_lt_or_lt_succ {n : } (p : Fin (n + 1)) (i : Fin n) :
                              theorem Fin.succ_le_or_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
                              theorem Fin.exists_castSucc_eq_of_ne_last {n : } {x : Fin (n + 1)} (h : x Fin.last n) :
                              ∃ (y : Fin n), Fin.castSucc y = x
                              theorem Fin.forall_fin_succ' {n : } {P : Fin (n + 1)Prop} :
                              (∀ (i : Fin (n + 1)), P i) (∀ (i : Fin n), P (Fin.castSucc i)) P (Fin.last n)
                              theorem Fin.eq_castSucc_or_eq_last {n : } (i : Fin (n + 1)) :
                              (∃ (j : Fin n), i = Fin.castSucc j) i = Fin.last n
                              theorem Fin.exists_fin_succ' {n : } {P : Fin (n + 1)Prop} :
                              (∃ (i : Fin (n + 1)), P i) (∃ (i : Fin n), P (Fin.castSucc i)) P (Fin.last n)
                              @[simp]
                              theorem Fin.castSucc_zero' {n : } [NeZero n] :

                              The Fin.castSucc_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                              theorem Fin.castSucc_pos' {n : } [NeZero n] {i : Fin n} (h : 0 < i) :

                              castSucc i is positive when i is positive.

                              The Fin.castSucc_pos in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                              @[simp]
                              theorem Fin.castSucc_eq_zero_iff' {n : } [NeZero n] (a : Fin n) :

                              The Fin.castSucc_eq_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                              theorem Fin.castSucc_ne_zero_iff' {n : } [NeZero n] (a : Fin n) :

                              The Fin.castSucc_ne_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                              theorem Fin.castSucc_ne_zero_of_lt {n : } {p : Fin n} {i : Fin n} (h : p < i) :
                              theorem Fin.succ_ne_last_iff {n : } (a : Fin (n + 1)) :
                              theorem Fin.succ_ne_last_of_lt {n : } {p : Fin n} {i : Fin n} (h : i < p) :
                              @[simp]
                              theorem Fin.coe_eq_castSucc {n : } {a : Fin n} :
                              a = Fin.castSucc a
                              theorem Fin.coe_succ_lt_iff_lt {n : } {j : Fin n} {k : Fin n} :
                              j < k j < k
                              @[simp]
                              theorem Fin.range_castSucc {n : } :
                              Set.range Fin.castSucc = {i : Fin (Nat.succ n) | i < n}
                              @[simp]
                              theorem Fin.coe_of_injective_castSucc_symm {n : } (i : Fin (Nat.succ n)) (hi : i Set.range Fin.castSucc) :
                              ((Equiv.ofInjective Fin.castSucc ).symm { val := i, property := hi }) = i
                              theorem Fin.strictMono_addNat {n : } (m : ) :
                              StrictMono fun (x : Fin n) => Fin.addNat x m
                              @[simp]
                              theorem Fin.addNatEmb_toEmbedding {n : } (m : ) :
                              (Fin.addNatEmb m).toEmbedding = { toFun := fun (x : Fin n) => Fin.addNat x m, inj' := }
                              @[simp]
                              theorem Fin.addNatEmb_apply {n : } (m : ) :
                              ∀ (x : Fin n), (Fin.addNatEmb m) x = Fin.addNat x m
                              def Fin.addNatEmb {n : } (m : ) :
                              Fin n ↪o Fin (n + m)

                              Fin.addNat as an OrderEmbedding, addNatEmb m i adds m to i, generalizes Fin.succ.

                              Equations
                              Instances For
                                @[simp]
                                theorem Fin.natAddEmb_apply (n : ) {m : } (i : Fin m) :
                                @[simp]
                                theorem Fin.natAddEmb_toEmbedding (n : ) {m : } :
                                (Fin.natAddEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := }
                                def Fin.natAddEmb (n : ) {m : } :
                                Fin m ↪o Fin (n + m)

                                Fin.natAdd as an OrderEmbedding, natAddEmb n i adds n to i "on the left".

                                Equations
                                Instances For

                                  pred #

                                  theorem Fin.strictMono_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : StrictMono f) :
                                  StrictMono fun (a : α) => Fin.pred (f a)
                                  theorem Fin.monotone_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : Monotone f) :
                                  Monotone fun (a : α) => Fin.pred (f a)
                                  theorem Fin.pred_one' {n : } [NeZero n] (h : optParam (1 0) ) :
                                  Fin.pred 1 h = 0
                                  theorem Fin.pred_last {n : } (h : optParam (Fin.last (n + 1) 0) ) :
                                  theorem Fin.pred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                                  Fin.pred i hi < j i < Fin.succ j
                                  theorem Fin.lt_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                                  j < Fin.pred i hi Fin.succ j < i
                                  theorem Fin.pred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                                  theorem Fin.le_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                                  theorem Fin.castSucc_pred_eq_pred_castSucc {n : } {a : Fin (n + 1)} (ha : a 0) (ha' : optParam (Fin.castSucc a 0) ) :
                                  theorem Fin.castSucc_pred_add_one_eq {n : } {a : Fin (n + 1)} (ha : a 0) :
                                  theorem Fin.le_pred_castSucc_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.castSucc a 0) :
                                  theorem Fin.pred_castSucc_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.castSucc a 0) :
                                  theorem Fin.pred_castSucc_lt {n : } {a : Fin (n + 1)} (ha : Fin.castSucc a 0) :
                                  theorem Fin.le_castSucc_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
                                  theorem Fin.castSucc_pred_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
                                  theorem Fin.castSucc_pred_lt {n : } {a : Fin (n + 1)} (ha : a 0) :
                                  @[inline]
                                  def Fin.castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                                  Fin n

                                  castPred i sends i : Fin (n + 1) to Fin n as long as i ≠ last n.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Fin.castLT_eq_castPred {n : } (i : Fin (n + 1)) (h : i < Fin.last n) (h' : optParam (i Fin.last n) ) :
                                    @[simp]
                                    theorem Fin.coe_castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                                    (Fin.castPred i h) = i
                                    @[simp]
                                    theorem Fin.castPred_castSucc {n : } {i : Fin n} (h' : optParam (Fin.castSucc i Fin.last n) ) :
                                    @[simp]
                                    theorem Fin.castSucc_castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                                    theorem Fin.castPred_eq_iff_eq_castSucc {n : } (i : Fin (n + 1)) (hi : i Fin.last n) (j : Fin n) :
                                    @[simp]
                                    theorem Fin.castPred_mk {n : } (i : ) (h₁ : i < n) (h₂ : optParam (i < Nat.succ n) ) (h₃ : optParam ({ val := i, isLt := h₂ } Fin.last n) ) :
                                    Fin.castPred { val := i, isLt := h₂ } h₃ = { val := i, isLt := h₁ }
                                    theorem Fin.castPred_le_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                    theorem Fin.castPred_lt_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                    theorem Fin.strictMono_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a Fin.last n) (hf₂ : StrictMono f) :
                                    StrictMono fun (a : α) => Fin.castPred (f a)
                                    theorem Fin.monotone_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a Fin.last n) (hf₂ : Monotone f) :
                                    Monotone fun (a : α) => Fin.castPred (f a)
                                    theorem Fin.castPred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                    theorem Fin.lt_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                    theorem Fin.castPred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                    theorem Fin.le_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                    theorem Fin.castPred_inj {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                    theorem Fin.castPred_zero' {n : } [NeZero n] (h : optParam (0 Fin.last n) ) :
                                    theorem Fin.castPred_zero {n : } (h : optParam (0 Fin.last (n + 1)) ) :
                                    @[simp]
                                    theorem Fin.castPred_one {n : } [NeZero n] (h : optParam (1 Fin.last (n + 1)) ) :
                                    theorem Fin.rev_pred :
                                    ∀ {a : } {i : Fin (a + 1)} (h : i 0) (h' : optParam (Fin.rev i Fin.last a) ), Fin.rev (Fin.pred i h) = Fin.castPred (Fin.rev i) h'
                                    theorem Fin.rev_castPred {n : } {i : Fin (n + 1)} (h : i Fin.last n) (h' : optParam (Fin.rev i 0) ) :
                                    theorem Fin.succ_castPred_eq_castPred_succ {n : } {a : Fin (n + 1)} (ha : a Fin.last n) (ha' : optParam (Fin.succ a Fin.last (n + 1)) ) :
                                    theorem Fin.succ_castPred_eq_add_one {n : } {a : Fin (n + 1)} (ha : a Fin.last n) :
                                    theorem Fin.castpred_succ_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.succ a Fin.last (n + 1)) :
                                    theorem Fin.lt_castPred_succ_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.succ a Fin.last (n + 1)) :
                                    theorem Fin.lt_castPred_succ {n : } {a : Fin (n + 1)} (ha : Fin.succ a Fin.last (n + 1)) :
                                    theorem Fin.succ_castPred_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) :
                                    theorem Fin.lt_succ_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) :
                                    theorem Fin.lt_succ_castPred {n : } {a : Fin (n + 1)} (ha : a Fin.last n) :
                                    theorem Fin.castPred_le_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) (hb : b 0) :
                                    Fin.castPred a ha Fin.pred b hb a < b
                                    theorem Fin.pred_lt_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) (hb : b Fin.last n) :
                                    Fin.pred a ha < Fin.castPred b hb a b
                                    theorem Fin.pred_lt_castPred {n : } {a : Fin (n + 1)} (h₁ : a 0) (h₂ : a Fin.last n) :
                                    Fin.pred a h₁ < Fin.castPred a h₂
                                    def Fin.divNat {n : } {m : } (i : Fin (m * n)) :
                                    Fin m

                                    Compute i / n, where n is a Nat and inferred the type of i.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Fin.coe_divNat {n : } {m : } (i : Fin (m * n)) :
                                      (Fin.divNat i) = i / n
                                      def Fin.modNat {n : } {m : } (i : Fin (m * n)) :
                                      Fin n

                                      Compute i % n, where n is a Nat and inferred the type of i.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Fin.coe_modNat {n : } {m : } (i : Fin (m * n)) :
                                        (Fin.modNat i) = i % n
                                        theorem Fin.modNat_rev {n : } {m : } (i : Fin (m * n)) :

                                        recursion and induction principles #

                                        theorem Fin.liftFun_iff_succ {n : } {α : Type u_1} (r : ααProp) [IsTrans α r] {f : Fin (n + 1)α} :
                                        ((fun (x x_1 : Fin (n + 1)) => x < x_1) r) f f ∀ (i : Fin n), r (f (Fin.castSucc i)) (f (Fin.succ i))
                                        theorem Fin.strictMono_iff_lt_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
                                        StrictMono f ∀ (i : Fin n), f (Fin.castSucc i) < f (Fin.succ i)

                                        A function f on Fin (n + 1) is strictly monotone if and only if f i < f (i + 1) for all i.

                                        theorem Fin.monotone_iff_le_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
                                        Monotone f ∀ (i : Fin n), f (Fin.castSucc i) f (Fin.succ i)

                                        A function f on Fin (n + 1) is monotone if and only if f i ≤ f (i + 1) for all i.

                                        theorem Fin.strictAnti_iff_succ_lt {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
                                        StrictAnti f ∀ (i : Fin n), f (Fin.succ i) < f (Fin.castSucc i)

                                        A function f on Fin (n + 1) is strictly antitone if and only if f (i + 1) < f i for all i.

                                        theorem Fin.antitone_iff_succ_le {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
                                        Antitone f ∀ (i : Fin n), f (Fin.succ i) f (Fin.castSucc i)

                                        A function f on Fin (n + 1) is antitone if and only if f (i + 1) ≤ f i for all i.

                                        instance Fin.neg (n : ) :
                                        Neg (Fin n)

                                        Negation on Fin n

                                        Equations
                                        • Fin.neg n = { neg := fun (a : Fin n) => { val := (n - a) % n, isLt := } }
                                        instance Fin.addCommGroup (n : ) [NeZero n] :

                                        Abelian group structure on Fin n.

                                        Equations

                                        Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

                                        Equations

                                        Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

                                        Equations
                                        • =

                                        Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

                                        Equations

                                        Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

                                        Equations
                                        theorem Fin.coe_neg {n : } (a : Fin n) :
                                        (-a) = (n - a) % n
                                        theorem Fin.eq_zero (n : Fin 1) :
                                        n = 0
                                        Equations
                                        @[simp]
                                        theorem Fin.coe_fin_one (a : Fin 1) :
                                        a = 0
                                        theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i 0) :
                                        i = 1
                                        @[simp]
                                        theorem Fin.coe_neg_one {n : } :
                                        (-1) = n
                                        theorem Fin.coe_sub_one {n : } (a : Fin (n + 1)) :
                                        (a - 1) = if a = 0 then n else a - 1
                                        @[simp]
                                        theorem Fin.lt_sub_one_iff {n : } {k : Fin (n + 2)} :
                                        k < k - 1 k = 0
                                        @[simp]
                                        theorem Fin.le_sub_one_iff {n : } {k : Fin (n + 1)} :
                                        k k - 1 k = 0
                                        @[simp]
                                        theorem Fin.sub_one_lt_iff {n : } {k : Fin (n + 1)} :
                                        k - 1 < k 0 < k
                                        theorem Fin.last_sub {n : } (i : Fin (n + 1)) :
                                        theorem Fin.add_one_le_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
                                        a + 1 b
                                        theorem Fin.exists_eq_add_of_le {n : } {a : Fin n} {b : Fin n} (h : a b) :
                                        ∃ k ≤ b, b = a + k
                                        theorem Fin.exists_eq_add_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
                                        ∃ k < b, k + 1 b b = a + k + 1
                                        @[simp]
                                        theorem Fin.neg_last (n : ) :
                                        theorem Fin.neg_nat_cast_eq_one (n : ) :
                                        -n = 1
                                        theorem Fin.pos_of_ne_zero {n : } {a : Fin (n + 1)} (h : a 0) :
                                        0 < a
                                        @[simp]
                                        theorem Fin.coe_ofNat_eq_mod (m : ) (n : ) [NeZero m] :
                                        n = n % m

                                        mul #

                                        theorem Fin.mul_one' {n : } [NeZero n] (k : Fin n) :
                                        k * 1 = k
                                        theorem Fin.one_mul' {n : } [NeZero n] (k : Fin n) :
                                        1 * k = k
                                        theorem Fin.mul_zero' {n : } [NeZero n] (k : Fin n) :
                                        k * 0 = 0
                                        theorem Fin.zero_mul' {n : } [NeZero n] (k : Fin n) :
                                        0 * k = 0
                                        instance Fin.toExpr (n : ) :
                                        Equations
                                        • One or more equations did not get rendered due to their size.